--- a/src/Pure/Tools/build.ML Fri May 17 20:30:04 2013 +0200
+++ b/src/Pure/Tools/build.ML Fri May 17 20:41:45 2013 +0200
@@ -114,7 +114,6 @@
|> Unsynchronized.setmp Multithreading.max_threads (Options.int options "threads")
|> Unsynchronized.setmp Future.ML_statistics true
|> no_document options ? Present.no_document
- |> Unsynchronized.setmp quick_and_dirty (Options.bool options "quick_and_dirty")
|> Unsynchronized.setmp Goal.skip_proofs (Options.bool options "skip_proofs")
|> Unsynchronized.setmp Pretty.margin_default (Options.int options "pretty_margin")
|> Unsynchronized.setmp Toplevel.timing (Options.bool options "timing");