--- a/src/Pure/System/build.ML Mon Sep 10 09:57:21 2012 +0200
+++ b/src/Pure/System/build.ML Mon Sep 10 12:00:28 2012 +0200
@@ -71,6 +71,12 @@
(case duplicates (op =) (map fst document_variants) of
[] => ()
| dups => error ("Duplicate document variants: " ^ commas_quote dups));
+
+ val _ =
+ if Options.string options "document_dump" = "" then ()
+ else
+ Output.physical_stderr
+ "### Legacy feature: old option \"document_dump\" -- use \"document_output\" instead\n";
val _ =
Session.init do_output false
(Options.bool options "browser_info") browser_info