> Am 05.08.2018 um 08:09 schrieb Gyan Doshi <gyandoshi at gmail.com>: > > Don't know if micro bump is needed. You may (should) always bump micro when the behaviour changes, if this counts as a change is up to you (the options you remove didn’t work before afaiu). Carl Eugen