Am 20.05.2018 um 20:46 schrieb Sven Schreiber:
Pushed. BTW, this was one of the cases where the simple
pull-edit-commit-push cycle for dummies didn't work, because a change
in the git repo (by Allin I think) made another pull with an automatic
merge necessary. Fortunately the auto merge went fine (I think).
Also, where is the changelog kept in the sources? It's not obvious to me.
thanks,
sven