a ksh script, and no longer has a dotty.ksh. Moved dotty.sh to dotty.ksh, and restored old vanilla dotty.sh.