--- a/src/Pure/Admin/build_doc.scala Sat Nov 10 07:57:20 2018 +0000
+++ b/src/Pure/Admin/build_doc.scala Sat Nov 10 14:08:02 2018 +0100
@@ -105,5 +105,5 @@
build_doc(options, progress, all_docs, max_jobs, system_mode, docs)
}
sys.exit(rc)
- }, admin = true)
+ })
}