# HG changeset patch
# User wenzelm
# Date 1219605344 -7200
# Node ID a4fdc97cd2ffe224c16d9bf1f640ff29306a50ae
# Parent  efc6d38d16d2d35680c1410efe50f5e6cd121652
get: allow null;

diff -r efc6d38d16d2 -r a4fdc97cd2ff src/Pure/General/position.scala
--- a/src/Pure/General/position.scala	Sun Aug 24 19:24:27 2008 +0200
+++ b/src/Pure/General/position.scala	Sun Aug 24 21:15:44 2008 +0200
@@ -13,7 +13,7 @@
 object Position {
 
   private def get_string(name: String, props: Properties) = {
-    val value = props.getProperty(name)
+    val value = if (props != null) props.getProperty(name) else null
     if (value != null) Some(value) else None
   }