--- a/src/Tools/jEdit/lib/Tools/jedit Tue Aug 14 10:44:03 2012 +0200
+++ b/src/Tools/jEdit/lib/Tools/jedit Tue Aug 14 11:37:58 2012 +0200
@@ -52,6 +52,7 @@
echo " -J OPTION add JVM runtime option"
echo " (default JEDIT_JAVA_OPTIONS=$JEDIT_JAVA_OPTIONS)"
echo " -b build only"
+ echo " -d DIR include session directory"
echo " -f fresh build"
echo " -j OPTION add jEdit runtime option"
echo " (default JEDIT_OPTIONS=$JEDIT_OPTIONS)"
@@ -82,13 +83,14 @@
BUILD_ONLY=false
BUILD_JARS="jars"
+JEDIT_SESSION_DIRS=""
JEDIT_LOGIC="$ISABELLE_LOGIC"
JEDIT_PRINT_MODE=""
function getoptions()
{
OPTIND=1
- while getopts "J:bdfj:l:m:" OPT
+ while getopts "J:bd:fj:l:m:" OPT
do
case "$OPT" in
J)
@@ -97,6 +99,13 @@
b)
BUILD_ONLY=true
;;
+ d)
+ if [ -z "$JEDIT_SESSION_DIRS" ]; then
+ JEDIT_SESSION_DIRS="$OPTARG"
+ else
+ JEDIT_SESSION_DIRS="$JEDIT_SESSION_DIRS:$OPTARG"
+ fi
+ ;;
f)
BUILD_JARS="jars_fresh"
;;
@@ -283,7 +292,7 @@
;;
esac
- export JEDIT_LOGIC JEDIT_PRINT_MODE
+ export JEDIT_SESSION_DIRS JEDIT_LOGIC JEDIT_PRINT_MODE
exec "$ISABELLE_TOOL" java "${JAVA_ARGS[@]}" \
-jar "$(jvmpath "$JEDIT_HOME/dist/jedit.jar")" \