build 487 B

123456789101112131415161718192021222324252627
  1. #!/bin/bash
  2. options==`getopt -o hps: --long pdf,html,stack-size: -n 'parse-options' -- "$@"`
  3. if [ $? != 0 ]; then
  4. echo "error"
  5. exit 1
  6. fi
  7. PDF=false
  8. HTML=false
  9. while true; do
  10. case "$1" in
  11. -p | --pdf ) PDF=true; shift ;;
  12. -h | --html ) HTML=true; shift ;;
  13. -s | --stack-size ) STACK_SIZE="$2"; shift; shift ;;
  14. -- ) shift; break ;;
  15. * ) break ;;
  16. esac
  17. done
  18. FILE=$@
  19. if [ "$PDF" = true ]; then scripts/make-pdf $FILE; fi
  20. if [ "$HTML" = true ]; then scripts/make-html $FILE; fi