make-doc.sh

   1 #!/bin/sh
   2
   3 pushd doc
   4 make all
   5 popd
   6 rm -rf docs
   7 mkdir docs
   8 mv doc/html docs
   9 mv doc/ctsim.htb docs
  10 mv doc/ctsim.pdf docs
  11 pushd doc
  12 make clean
  13 popd