# HG changeset patch
# User wenzelm
# Date 1314390341 -7200
# Node ID 2f0a34fc4d2d62642be449330a2f54e5c53fb539
# Parent  470f2ee5950e6307abc86d694463bbc6c571a7e9
back to tradition Scratch.thy default -- execution wrt. perspective overcomes the main problems of 226563829580;

diff -r 470f2ee5950e -r 2f0a34fc4d2d src/Tools/jEdit/lib/Tools/jedit
--- a/src/Tools/jEdit/lib/Tools/jedit	Fri Aug 26 22:14:12 2011 +0200
+++ b/src/Tools/jEdit/lib/Tools/jedit	Fri Aug 26 22:25:41 2011 +0200
@@ -134,11 +134,14 @@
 
 # args
 
-while [ "$#" -gt 0 ]
-do
-  ARGS["${#ARGS[@]}"]="$(jvmpath "$1")"
-  shift
-done
+if [ "$#" -eq 0 ]; then
+  ARGS["${#ARGS[@]}"]="Scratch.thy"
+else
+  while [ "$#" -gt 0 ]; do
+    ARGS["${#ARGS[@]}"]="$(jvmpath "$1")"
+    shift
+  done
+fi
 
 
 ## dependencies