# HG changeset patch
# User wenzelm
# Date 853158032 -3600
# Node ID 50abca9d40437041ea49ece2d7756cf218dd6480
# Parent  f5e2288c2697d6f5c9dd0770a60d3a60d8ae7fe8
added -? option;

diff -r f5e2288c2697 -r 50abca9d4043 bin/isatool
--- a/bin/isatool	Mon Jan 13 09:29:55 1997 +0100
+++ b/bin/isatool	Mon Jan 13 13:20:32 1997 +0100
@@ -48,7 +48,7 @@
 
 ## main
 
-[ $# -lt 1 ] && usage
+[ $# -lt 1 -o "$1" = "-?" ] && usage
 
 TOOL_BASE="$1"
 TOOL="$ISABELLE_HOME/lib/Tools/$1"