equal
deleted
inserted
replaced
111 def getenv_strict(name: String): String = |
111 def getenv_strict(name: String): String = |
112 { |
112 { |
113 val value = getenv(name) |
113 val value = getenv(name) |
114 if (value != "") value else error("Undefined environment variable: " + name) |
114 if (value != "") value else error("Undefined environment variable: " + name) |
115 } |
115 } |
|
116 |
|
117 override def toString = getenv("ISABELLE_HOME") |
116 |
118 |
117 |
119 |
118 /* file path specifications */ |
120 /* file path specifications */ |
119 |
121 |
120 private val Cygdrive = new Regex( |
122 private val Cygdrive = new Regex( |