src/Pure/Tools/build.ML
changeset 52059 2f970c7f722b
parent 52052 892061142ba6
child 52104 250cd2a9308d
     1.1 --- a/src/Pure/Tools/build.ML	Fri May 17 20:30:04 2013 +0200
     1.2 +++ b/src/Pure/Tools/build.ML	Fri May 17 20:41:45 2013 +0200
     1.3 @@ -114,7 +114,6 @@
     1.4      |> Unsynchronized.setmp Multithreading.max_threads (Options.int options "threads")
     1.5      |> Unsynchronized.setmp Future.ML_statistics true
     1.6      |> no_document options ? Present.no_document
     1.7 -    |> Unsynchronized.setmp quick_and_dirty (Options.bool options "quick_and_dirty")
     1.8      |> Unsynchronized.setmp Goal.skip_proofs (Options.bool options "skip_proofs")
     1.9      |> Unsynchronized.setmp Pretty.margin_default (Options.int options "pretty_margin")
    1.10      |> Unsynchronized.setmp Toplevel.timing (Options.bool options "timing");