# HG changeset patch
# User wenzelm
# Date 1478948802 -3600
# Node ID 271e98c1fa40fc3e1c80d7973759fcee14bcc45b
# Parent  234571db1b90d307a95eb04172238e0e0cfc2117
proper admin tool;

diff -r 234571db1b90 -r 271e98c1fa40 src/Pure/Admin/build_polyml.scala
--- a/src/Pure/Admin/build_polyml.scala	Sat Nov 12 11:19:30 2016 +0100
+++ b/src/Pure/Admin/build_polyml.scala	Sat Nov 12 12:06:42 2016 +0100
@@ -185,5 +185,5 @@
         build_polyml(root, sha1_root = sha1_root, progress = new Console_Progress,
           arch_64 = arch_64, options = options, other_bash = other_bash)
       }
-    })
+    }, admin = true)
 }