diff -r c4d16f35c6e7 -r b00508facb4f src/Pure/Tools/build.ML
--- 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