| changeset 26576 | fc76b7b79ba9 |
| parent 15847 | c05c7670f166 |
| child 28650 | a7ba12e0d3b7 |
| 26575:042617a1c86c | 26576:fc76b7b79ba9 |
|---|---|
43 [ "$#" -eq 0 -o "$1" = "-?" ] && usage |
43 [ "$#" -eq 0 -o "$1" = "-?" ] && usage |
44 |
44 |
45 |
45 |
46 ## main |
46 ## main |
47 |
47 |
48 #set by configure |
48 exec perl -w "$ISABELLE_HOME/lib/scripts/dimacs2hol.pl" "$@" |
49 AUTO_PERL=perl |
|
50 |
|
51 "$AUTO_PERL" -w "$ISABELLE_HOME/lib/scripts/dimacs2hol.pl" "$@" |