aboutsummaryrefslogtreecommitdiffhomepage
path: root/isar/interface
diff options
context:
space:
mode:
authorGravatar Makarius Wenzel <makarius@sketis.net>2001-08-31 22:22:13 +0000
committerGravatar Makarius Wenzel <makarius@sketis.net>2001-08-31 22:22:13 +0000
commit0816b51ece79bec07fcda3ef413355c032a16c6d (patch)
treeb36e4409612543aa49aa6aa8ab0b393728039b42 /isar/interface
parent976dcd83aee1757876c8d1aa313d5e00abcf0d52 (diff)
handle relative heap paths gracefully;
Diffstat (limited to 'isar/interface')
-rw-r--r--isar/interface8
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"