# HG changeset patch # User wenzelm # Date 1246045976 -7200 # Node ID 83cf912efd8a09473e74c03eca7efbdebca1cf10 # Parent 9ba00a9671211aaa3307fb8169a3ebc6876dfa69 default file is plain Scratch.thy (as in Proof General); diff -r 9ba00a967121 -r 83cf912efd8a src/Tools/jEdit/dist-template/interface --- a/src/Tools/jEdit/dist-template/interface Fri Jun 26 21:47:22 2009 +0200 +++ b/src/Tools/jEdit/dist-template/interface Fri Jun 26 21:52:56 2009 +0200 @@ -73,7 +73,7 @@ declare -a FILES=() if [ "$#" -eq 0 ]; then - FILES+=($(jvmpath "$HOME/Scratch.thy")) + FILES+=(Scratch.thy) else while [ "$#" -gt 0 ]; do FILES+=($(jvmpath "$1"))