getenv_strict needs to be based on getenv (accidentally broken in 0e88d33e8d19);
authorwenzelm
Sat, 23 May 2009 17:21:44 +0200
changeset 31234 6ce6801129de
parent 31233 c4c1692d4eee
child 31235 67c796138bf0
getenv_strict needs to be based on getenv (accidentally broken in 0e88d33e8d19);
src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Fri May 22 13:22:16 2009 -0700
+++ b/src/Pure/System/isabelle_system.scala	Sat May 23 17:21:44 2009 +0200
@@ -27,7 +27,7 @@
   }
 
   def getenv_strict(name: String) = {
-    val value = environment.get(name)
+    val value = getenv(name)
     if (value != "") value else error("Undefined environment variable: " + name)
   }