equal
deleted
inserted
replaced
98 { |
98 { |
99 echo |
99 echo |
100 echo "Usage: isabelle $PRG [OPTIONS] [FILES ...]" |
100 echo "Usage: isabelle $PRG [OPTIONS] [FILES ...]" |
101 echo |
101 echo |
102 echo " Options are:" |
102 echo " Options are:" |
103 echo " -A NAME ancestor session for options -R (default: parent)" |
103 echo " -A NAME ancestor session for option -R (default: parent)" |
104 echo " -D NAME=X set JVM system property" |
104 echo " -D NAME=X set JVM system property" |
105 echo " -J OPTION add JVM runtime option" |
105 echo " -J OPTION add JVM runtime option" |
106 echo " (default $JEDIT_JAVA_SYSTEM_OPTIONS $JEDIT_JAVA_OPTIONS)" |
106 echo " (default $JEDIT_JAVA_SYSTEM_OPTIONS $JEDIT_JAVA_OPTIONS)" |
107 echo " -R NAME build image with requirements from other sessions" |
107 echo " -R NAME build image with requirements from other sessions" |
108 echo " -b build only" |
108 echo " -b build only" |