author | boehmes |
Mon, 05 Sep 2011 14:17:44 +0200 | |
changeset 44719 | 176adba0c35e |
parent 44718 | b656af4c9796 |
child 44720 | f3a8c19708c8 |
--- a/src/Tools/jEdit/README_BUILD Mon Sep 05 11:34:54 2011 +0200 +++ b/src/Tools/jEdit/README_BUILD Mon Sep 05 14:17:44 2011 +0200 @@ -16,7 +16,7 @@ - JAVA_HOME - SCALA_HOME -- JEDIT_BUILD_HOME (via "init_component .../jedit_build...") +- ISABELLE_JEDIT_BUILD_HOME (via "init_component .../jedit_build...") Build and run