# HG changeset patch
# User wenzelm
# Date 935059363 -7200
# Node ID 7a2008de228dc05304c6687f778b0c366d404282
# Parent  3a001f2148f7391666a63e0c4a870ae6841c126d
really removed -m option;

diff -r 3a001f2148f7 -r 7a2008de228d lib/Tools/usedir
--- a/lib/Tools/usedir	Thu Aug 19 12:41:09 1999 +0200
+++ b/lib/Tools/usedir	Thu Aug 19 12:42:43 1999 +0200
@@ -20,7 +20,6 @@
   echo "    -b           build mode (output heap image, using current dir)"
   echo "    -i BOOL      generate theory browsing information,"
   echo "                 i.e. HTML / graph data (default false)"
-  echo "    -m BOOL      multi line output (default false)"
   echo "    -r           reset session path"
   echo "    -s NAME      override session NAME"
   echo
@@ -37,7 +36,6 @@
 
 BUILD=""
 INFO=false
-MULTI=false
 RESET=false
 SESSION=""
 RPATH=""
@@ -45,7 +43,7 @@
 function getoptions()
 {
   OPTIND=1
-  while getopts "BP:bi:m:rs:" OPT
+  while getopts "BP:bi:rs:" OPT
   do
     case "$OPT" in
       B)
@@ -58,9 +56,6 @@
       i)
         INFO="$OPTARG"
         ;;
-      m)
-        MULTI="$OPTARG"
-        ;;
       r)
         RESET=true
         ;;