option -d: enable debugger;
authorwenzelm
Tue, 01 Sep 2009 15:37:05 +0200
changeset 34691 f28c014bcbe3
parent 34690 e588fe99cd68
child 34692 3c0a8bece8b8
option -d: enable debugger;
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"
       ;;