# HG changeset patch
# User wenzelm
# Date 1343120689 -7200
# Node ID a7bf1587eba0b8cf1076b46aa784036311abc33b
# Parent  07f752935ececd6933e2210dcae5f8c5033ffeec
observe "quick_and_dirty";

diff -r 07f752935ece -r a7bf1587eba0 src/Pure/System/build.ML
--- a/src/Pure/System/build.ML	Tue Jul 24 11:02:42 2012 +0200
+++ b/src/Pure/System/build.ML	Tue Jul 24 11:04:49 2012 +0200
@@ -22,7 +22,8 @@
         (Options.int options "parallel_proofs_threshold")
     |> Unsynchronized.setmp Multithreading.trace (Options.int options "threads_trace")
     |> Unsynchronized.setmp Multithreading.max_threads (Options.int options "threads")
-    |> Options.bool options "no_document" ? Present.no_document;
+    |> Options.bool options "no_document" ? Present.no_document
+    |> Unsynchronized.setmp quick_and_dirty (Options.bool options "quick_and_dirty");
 
 fun build args_file =
   let