equal
deleted
inserted
replaced
16 echo |
16 echo |
17 echo " Options are:" |
17 echo " Options are:" |
18 echo " -c cleanup -- be aggressive in removing old stuff" |
18 echo " -c cleanup -- be aggressive in removing old stuff" |
19 echo " -o FORMAT specify output format: dvi (default), dvi.gz, ps," |
19 echo " -o FORMAT specify output format: dvi (default), dvi.gz, ps," |
20 echo " ps.gz, pdf" |
20 echo " ps.gz, pdf" |
21 echo " -v be verbose" |
|
22 echo |
21 echo |
23 echo " Prepare the theory session document in DIR (default 'document')" |
22 echo " Prepare the theory session document in DIR (default 'document')" |
24 echo " producing the specified output format." |
23 echo " producing the specified output format." |
25 echo |
24 echo |
26 exit 1 |
25 exit 1 |
37 |
36 |
38 # options |
37 # options |
39 |
38 |
40 CLEAN="" |
39 CLEAN="" |
41 OUTFORMAT=dvi |
40 OUTFORMAT=dvi |
42 VERBOSE="" |
|
43 |
41 |
44 while getopts "co:v" OPT |
42 while getopts "co:" OPT |
45 do |
43 do |
46 case "$OPT" in |
44 case "$OPT" in |
47 c) |
45 c) |
48 CLEAN=true |
46 CLEAN=true |
49 ;; |
47 ;; |
50 o) |
48 o) |
51 OUTFORMAT="$OPTARG" |
49 OUTFORMAT="$OPTARG" |
52 ;; |
|
53 v) |
|
54 VERBOSE=true |
|
55 ;; |
50 ;; |
56 \?) |
51 \?) |
57 usage |
52 usage |
58 ;; |
53 ;; |
59 esac |
54 esac |
120 "$ISATOOL" latex -o "$OUTFORMAT" |
115 "$ISATOOL" latex -o "$OUTFORMAT" |
121 RC="$?" |
116 RC="$?" |
122 fi |
117 fi |
123 |
118 |
124 if [ "$RC" -eq 0 -a -f "root.$OUTFORMAT" ]; then |
119 if [ "$RC" -eq 0 -a -f "root.$OUTFORMAT" ]; then |
125 cp -f "root.$OUTFORMAT" "../document.$OUTFORMAT" && \ |
120 cp -f "root.$OUTFORMAT" "../document.$OUTFORMAT" |
126 [ -n "$VERBOSE" ] && echo "$(cd ..; echo "Prepared $PWD/document.$OUTFORMAT")" >&2 |
|
127 fi |
121 fi |
128 |
122 |
129 exit "$RC" |
123 exit "$RC" |
130 ) |
124 ) |
131 RC="$?" |
125 RC="$?" |