# HG changeset patch
# User boehmes
# Date 1315225064 -7200
# Node ID 176adba0c35e51caf7c166149f6ed84c10398bf0
# Parent  b656af4c9796ad19db3ee6df2be3cc15d81bf09c
tuned

diff -r b656af4c9796 -r 176adba0c35e src/Tools/jEdit/README_BUILD
--- 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