General comment to the zsh scripts (and the corresponding bash scripts) and the maintenance burden: Wouldn't it be simpler (and more fun) to write a script that extracts and generates most of these files? doc/gendoc.py could be perhaps be used as a starting point. /Mads