--- a/src/Pure/Tools/build.ML Tue Oct 18 17:41:56 2016 +0200
+++ b/src/Pure/Tools/build.ML Wed Oct 19 14:42:28 2016 +0200
@@ -114,6 +114,12 @@
symbols = symbols,
last_timing = last_timing,
master_dir = master_dir}
+ |>
+ (case Options.string options "profiling" of
+ "" => I
+ | "time" => profile_time
+ | "allocations" => profile_allocations
+ | bad => error ("Bad profiling option: " ^ quote bad))
|> Unsynchronized.setmp print_mode
(space_explode "," (Options.string options "print_mode") @ print_mode_value ())) thys)
else