diff options
author | Makarius Wenzel <makarius@sketis.net> | 2001-08-31 22:22:13 +0000 |
---|---|---|
committer | Makarius Wenzel <makarius@sketis.net> | 2001-08-31 22:22:13 +0000 |
commit | 0816b51ece79bec07fcda3ef413355c032a16c6d (patch) | |
tree | b36e4409612543aa49aa6aa8ab0b393728039b42 /isar/interface | |
parent | 976dcd83aee1757876c8d1aa313d5e00abcf0d52 (diff) |
handle relative heap paths gracefully;
Diffstat (limited to 'isar/interface')
-rw-r--r-- | isar/interface | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/isar/interface b/isar/interface index 46ac8a7f..71a922f5 100644 --- a/isar/interface +++ b/isar/interface @@ -161,6 +161,14 @@ do [ -f "$FILE" ] && ARGS="$ARGS -l '$FILE'" done +case "$LOGIC" in + /*) + ;; + */*) + LOGIC="$PWD/$LOGIC" + ;; +esac + PROOFGENERAL_HOME="$SUPER" PROOFGENERAL_ASSISTANTS="$KIND" PROOFGENERAL_LOGIC="$LOGIC" |