Next Stop merging master 23

Merging master anyway

Just stop using git-pull all the time



Next Copyright © 2013 M. J. Dominus