> Ich nehme sie raus, denn ohne Dollars tuts (also nicht generell,
> aber in diesem Falle schon).
Wie Du gemerkt hast, habe ich dieses Artefakt von Günters
regexp-Durchläufen bereits entfernt, und wir haben einen unnötigen
»Merge« im git-Repositorium. Aus diesem Grunde bitte vor »git push«
unbedingt »git pull --rebase« ausführen!
Werner