diff -r a825c5929f4f -r f91212fd2c7c lib/scripts/isa-xterm
--- a/lib/scripts/isa-xterm	Wed Nov 25 14:06:13 1998 +0100
+++ b/lib/scripts/isa-xterm	Wed Nov 25 14:07:22 1998 +0100
@@ -42,27 +42,34 @@
 PASS=""
 SYMBOLS="true"
 
-while getopts "g:h:p:s:" OPT
-do
-  case "$OPT" in
-    g)
-      MAINGEOM="$OPTARG"
-      ;;
-    h)
-      HILITE="$OPTARG"
-      ;;
-    p)
-      PASS="$PASS $OPTARG"
-      ;;
-    s)
-      SYMBOLS="$OPTARG"
-      ;;
-    \?)
-      usage
-      ;;
-  esac
-done
+function getoptions()
+{
+  OPTIND=1
+  while getopts "g:h:p:s:" OPT
+  do
+    case "$OPT" in
+      g)
+        MAINGEOM="$OPTARG"
+        ;;
+      h)
+        HILITE="$OPTARG"
+        ;;
+      p)
+        PASS="$PASS $OPTARG"
+        ;;
+      s)
+        SYMBOLS="$OPTARG"
+        ;;
+      \?)
+        usage
+        ;;
+    esac
+  done
+}
 
+getoptions $ISABELLE_XTERM_OPTIONS
+
+getoptions "$@"
 shift $(($OPTIND - 1))