author | wenzelm |
Sat, 08 Sep 2001 20:00:31 +0200 | |
changeset 11550 | 915c5de6480f |
parent 10905 | e23abeef8150 |
child 11566 | 94d2d6531c57 |
permissions | -rwxr-xr-x |
10555 | 1 |
#!/usr/bin/env bash |
2292 | 2 |
# |
2308 | 3 |
# $Id$ |
9786 | 4 |
# Author: Markus Wenzel, TU Muenchen |
5 |
# License: GPL (GNU GENERAL PUBLIC LICENSE) |
|
2308 | 6 |
# |
11550
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
10905
diff
changeset
|
7 |
# Smart selection of isabelle-process versus isabelle-interface. |
2292 | 8 |
|
11550
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
10905
diff
changeset
|
9 |
THIS=$(cd "$(dirname "$0")"; pwd) |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
10905
diff
changeset
|
10 |
NAME="$(basename "$0")" |
2292 | 11 |
|
11550
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
10905
diff
changeset
|
12 |
PRG=isabelle-interface |
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
10905
diff
changeset
|
13 |
[ "$NAME" = isabelle ] && PRG=isabelle-process |
9786 | 14 |
|
11550
915c5de6480f
smart selection of isabelle-process versus isabelle-interface;
wenzelm
parents:
10905
diff
changeset
|
15 |
exec "$THIS/$PRG" "$@" |