# HG changeset patch
# User wenzelm
# Date 1342799035 -7200
# Node ID 10b534e6420954f40ab7abf7332a13272b364e9f
# Parent  dc538eef2cf20af89c8a70c4e77d802121c3769d
tuned signature;

diff -r dc538eef2cf2 -r 10b534e64209 src/Pure/System/options.scala
--- a/src/Pure/System/options.scala	Fri Jul 20 16:47:43 2012 +0200
+++ b/src/Pure/System/options.scala	Fri Jul 20 17:43:55 2012 +0200
@@ -149,13 +149,20 @@
     result
   }
 
+  def define(name: String, opt_value: Option[String]): Options =
+  {
+    val opt = check_name(name)
+    opt_value match {
+      case Some(value) => define(name, value)
+      case None if opt.typ == Options.Bool => define(name, "true")
+      case None => error("Missing value for option " + quote(name) + " : " + opt.typ.print)
+    }
+  }
+
   def define_simple(str: String): Options =
   {
     str.indexOf('=') match {
-      case -1 =>
-        val opt = check_name(str)
-        if (opt.typ == Options.Bool) define(str, "true")
-        else error("Missing value for option " + quote(str) + " : " + opt.typ.print)
+      case -1 => define(str, None)
       case i => define(str.substring(0, i), str.substring(i + 1))
     }
   }