diff -r 3d954183b707 -r 258bef08b31e src/Pure/Admin/check_sources.scala --- 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) + }) }