--- a/src/Pure/Admin/check_sources.scala Sat Nov 10 07:57:20 2018 +0000
+++ b/src/Pure/Admin/check_sources.scala Sat Nov 10 14:08:02 2018 +0100
@@ -70,5 +70,5 @@
if (specs.isEmpty) getopts.usage()
for (root <- specs) check_hg(Path.explode(root))
- }, admin = true)
+ })
}