equal
deleted
inserted
replaced
|
1 #!/bin/bash -norc |
|
2 # |
|
3 # $Id$ |
|
4 # |
|
5 # DESCRIPTION: use dir without committing into database |
|
6 |
|
7 |
|
8 PRG=$(basename $0) |
|
9 |
|
10 function usage() |
|
11 { |
|
12 echo |
|
13 echo "Usage: $PRG LOGIC DIR" |
|
14 echo |
|
15 echo " Use dir without committing into database (FIXME ISABELLE_HTML)." |
|
16 echo |
|
17 exit 1 |
|
18 } |
|
19 |
|
20 |
|
21 ## args |
|
22 |
|
23 [ $# -ne 2 ] && usage |
|
24 |
|
25 LOGIC="$1"; shift |
|
26 DIR="$1"; shift |
|
27 |
|
28 |
|
29 ## main |
|
30 |
|
31 exec $ISABELLE \ |
|
32 -e "make_html := $ISABELLE_HTML;" \ |
|
33 -e "exit_use_dir\"$DIR\"; quit();" \ |
|
34 -rq $LOGIC |