src/Tools/jEdit/README_BUILD
changeset 45590 176adba0c35e
parent 45577 f4b42f310f86
child 46021 cf6a5de94bfc
     1.1 --- a/src/Tools/jEdit/README_BUILD	Mon Sep 05 11:34:54 2011 +0200
     1.2 +++ b/src/Tools/jEdit/README_BUILD	Mon Sep 05 14:17:44 2011 +0200
     1.3 @@ -16,7 +16,7 @@
     1.4  
     1.5  - JAVA_HOME
     1.6  - SCALA_HOME
     1.7 -- JEDIT_BUILD_HOME (via "init_component .../jedit_build...")
     1.8 +- ISABELLE_JEDIT_BUILD_HOME (via "init_component .../jedit_build...")
     1.9  
    1.10  
    1.11  Build and run