equal
deleted
inserted
replaced
11 { |
11 { |
12 echo |
12 echo |
13 echo "Usage: $PRG [OPTIONS] [DIR]" |
13 echo "Usage: $PRG [OPTIONS] [DIR]" |
14 echo |
14 echo |
15 echo " Options are:" |
15 echo " Options are:" |
16 echo " -c remove DIR after succesful run (!)" |
16 echo " -c cleanup -- be aggressive in removing old stuff" |
17 echo " -o FORMAT specify output format: dvi (default), dvi.gz, ps," |
17 echo " -o FORMAT specify output format: dvi (default), dvi.gz, ps," |
18 echo " ps.gz, pdf" |
18 echo " ps.gz, pdf" |
19 echo |
19 echo |
20 echo " Prepare the theory session document in DIR (default 'document')" |
20 echo " Prepare the theory session document in DIR (default 'document')" |
21 echo " producing the specified output format." |
21 echo " producing the specified output format." |
79 # prepare document |
79 # prepare document |
80 |
80 |
81 function pre_latex () |
81 function pre_latex () |
82 { |
82 { |
83 local FMT="$1" |
83 local FMT="$1" |
84 rm -f *.aux *.out |
84 [ -n "$CLEAN" ] && rm -f *.aux *.out |
85 if [ -f root.bib ] |
85 if [ -f root.bib ] |
86 then |
86 then |
87 $ISATOOL latex -o "$FMT" && \ |
87 $ISATOOL latex -o "$FMT" && \ |
88 $ISATOOL latex -o bbl && \ |
88 $ISATOOL latex -o bbl && \ |
89 $ISATOOL latex -o "$FMT" |
89 $ISATOOL latex -o "$FMT" |
92 fi |
92 fi |
93 } |
93 } |
94 |
94 |
95 ( |
95 ( |
96 cd "$DIR" || fail "Bad directory '$DIR'" |
96 cd "$DIR" || fail "Bad directory '$DIR'" |
|
97 |
|
98 [ -n "$CLEAN" ] && rm -f "../document.$OUTFORMAT" |
97 |
99 |
98 if [ -f IsaMakefile ]; then |
100 if [ -f IsaMakefile ]; then |
99 $ISATOOL make "$OUTFORMAT" |
101 $ISATOOL make "$OUTFORMAT" |
100 RC=$? |
102 RC=$? |
101 elif [ "$OUTFORMAT" = pdf ]; then |
103 elif [ "$OUTFORMAT" = pdf ]; then |