make_pdf.sh

   1 #!/bin/sh
   2 # Creates a PDF version of the wiki.
   3
   4 echo "making PDF"
   5
   6 ./make_html_single.sh
   7
   8 cat lrs_wiki.html | sed "s/<code> /<code>\n /" > _tmp.html
   9 htmldoc --bodyfont sans --fontsize 10 --gray --left 8mm --right 8mm --top 8mm --bottom 8mm --continuous --header ... --header1 ... --footer ct/ -t pdf -f lrs_wiki.pdf _tmp.html
  10 rm _tmp.html
  11
  12 echo "done"