author | wenzelm |
Sat, 20 Dec 2008 12:17:43 +0100 | |
changeset 34414 | de921b3cb263 |
parent 34413 | 10cdbba5af89 |
child 34415 | 3f76ce248c0e |
--- a/src/Tools/jEdit/makedist Sat Dec 20 11:07:02 2008 +0100 +++ b/src/Tools/jEdit/makedist Sat Dec 20 12:17:43 2008 +0100 @@ -11,7 +11,7 @@ ## diagnostics -JEDIT_HOME="/home/isajedit/jedit-orig/4.3pre15" +JEDIT_HOME="/home/isajedit/jedit-orig/4.3pre16" SCALA_HOME="/home/scala/current" function usage()