equal
deleted
inserted
replaced
|
1 #!/bin/bash |
|
2 # |
|
3 # $Id$ |
|
4 # |
|
5 # DESCRIPTION: prepare theory session document |
|
6 |
|
7 |
|
8 PRG=$(basename $0) |
|
9 |
|
10 function usage() |
|
11 { |
|
12 echo |
|
13 echo "Usage: $PRG [OPTIONS] [DIR]" |
|
14 echo |
|
15 echo " Options are:" |
|
16 echo " -o FORMAT specify output format: dvi (default), dvi.gz, ps, ps.gz, pdf" |
|
17 echo |
|
18 echo |
|
19 echo " Prepare the theory session document in DIR (default .)" |
|
20 echo " producing the speficied output format." |
|
21 echo |
|
22 exit 1 |
|
23 } |
|
24 |
|
25 function fail() |
|
26 { |
|
27 echo "$1" >&2 |
|
28 exit 2 |
|
29 } |
|
30 |
|
31 |
|
32 ## process command line |
|
33 |
|
34 # options |
|
35 |
|
36 OUTFORMAT=dvi |
|
37 |
|
38 while getopts "o:" OPT |
|
39 do |
|
40 case "$OPT" in |
|
41 o) |
|
42 OUTFORMAT="$OPTARG" |
|
43 ;; |
|
44 \?) |
|
45 usage |
|
46 ;; |
|
47 esac |
|
48 done |
|
49 |
|
50 shift $(($OPTIND - 1)) |
|
51 |
|
52 |
|
53 # args |
|
54 |
|
55 DIR="." |
|
56 [ $# -ge 1 ] && { DIR="$1"; shift; } |
|
57 |
|
58 [ $# -ne 0 ] && usage |
|
59 |
|
60 |
|
61 ## main |
|
62 |
|
63 #prepare document |
|
64 |
|
65 cd "$DIR" || fail "Bad directory '$DIR'" |
|
66 |
|
67 if [ -f IsaMakefile ]; then |
|
68 $ISATOOL make "$OUTFORMAT" |
|
69 RC=$? #FIXME !?? |
|
70 elif [ "$OUTFORMAT" = pdf ]; then |
|
71 $ISATOOL latex -o pdf && $ISATOOL latex -o pdf |
|
72 RC=$? |
|
73 else |
|
74 $ISATOOL latex -o dvi && $ISATOOL latex -o "$OUTFORMAT" |
|
75 RC=$? |
|
76 fi |
|
77 |
|
78 |
|
79 #install |
|
80 |
|
81 [ "$RC" -gt 0 -o ! -f "root.$OUTFORMAT" ] && fail "Failed to prepare document in directory '$DIR'" |
|
82 cp -f "root.$OUTFORMAT" "../document.$OUTFORMAT" |