# HG changeset patch # User wenzelm # Date 1251812225 -7200 # Node ID f28c014bcbe3cfc101011e1991c0ff44fa9095c0 # Parent e588fe99cd685b64f299b89d41a8426ea24a8c0b option -d: enable debugger; diff -r e588fe99cd68 -r f28c014bcbe3 src/Tools/jEdit/dist-template/lib/Tools/jedit --- a/src/Tools/jEdit/dist-template/lib/Tools/jedit Tue Sep 01 15:12:24 2009 +0200 +++ b/src/Tools/jEdit/dist-template/lib/Tools/jedit Tue Sep 01 15:37:05 2009 +0200 @@ -17,6 +17,7 @@ echo " Options are:" echo " -J OPTION add JVM runtime option" echo " (default JEDIT_JAVA_OPTIONS=$JEDIT_JAVA_OPTIONS)" + echo " -d enable debugger" echo " -j OPTION add jEdit runtime option" echo " (default JEDIT_OPTIONS=$JEDIT_OPTIONS)" echo " -l NAME logic image name (default ISABELLE_LOGIC=$ISABELLE_LOGIC)" @@ -45,12 +46,16 @@ declare -a JAVA_OPTIONS; eval "JAVA_OPTIONS=($JEDIT_JAVA_OPTIONS)" declare -a OPTIONS; eval "OPTIONS=($JEDIT_OPTIONS)" -while getopts "J:j:l:m:" OPT +while getopts "J:dj:l:m:" OPT do case "$OPT" in J) JAVA_OPTIONS["${#JAVA_OPTIONS[@]}"]="$OPTARG" ;; + d) + JAVA_OPTIONS["${#JAVA_OPTIONS[@]}"]="-Xdebug" + JAVA_OPTIONS["${#JAVA_OPTIONS[@]}"]="-Xrunjdwp:transport=dt_socket,server=y,suspend=n" + ;; j) OPTIONS["${#OPTIONS[@]}"]="$OPTARG" ;;