merged
authorwenzelm
Mon, 13 Aug 2012 20:31:24 +0200
changeset 48789 7476665f3e0f
parent 48788 cea7f88c8084 (diff)
parent 48787 ab3e7f40f341 (current diff)
child 48790 6e739225dd8a
child 48796 0f94b8b69e79
merged
src/Tools/jEdit/patches/jedit-4.5.1/caret
src/Tools/jEdit/patches/jedit-4.5.1/extended_styles
src/Tools/jEdit/patches/jedit-4.5.1/macos
src/Tools/jEdit/patches/jedit-4.5.1/memory
--- a/Admin/download-components	Mon Aug 13 19:51:48 2012 +0200
+++ b/Admin/download-components	Mon Aug 13 20:31:24 2012 +0200
@@ -17,7 +17,7 @@
   exit 1
 }
 
-ISABELLE_HOME_USER="$(isabelle getenv -b ISABELLE_HOME_USER)"
+ISABELLE_HOME_USER="$("${HERE}/../bin/isabelle" getenv -b ISABELLE_HOME_USER)"
 : ${TMP:='/tmp'}
 REMOTE='http://isabelle.in.tum.de/components'
 LOCAL="${ISABELLE_HOME_USER}/contrib"