123456789101112131415161718192021222324252627 |
- #!/bin/bash
- options==`getopt -o hps: --long pdf,html,stack-size: -n 'parse-options' -- "$@"`
- if [ $? != 0 ]; then
- echo "error"
- exit 1
- fi
- PDF=false
- HTML=false
- while true; do
- case "$1" in
- -p | --pdf ) PDF=true; shift ;;
- -h | --html ) HTML=true; shift ;;
- -s | --stack-size ) STACK_SIZE="$2"; shift; shift ;;
- -- ) shift; break ;;
- * ) break ;;
- esac
- done
- FILE=$@
- if [ "$PDF" = true ]; then scripts/make-pdf $FILE; fi
- if [ "$HTML" = true ]; then scripts/make-html $FILE; fi
|