tuned output;
authorwenzelm
Tue, 11 Oct 2016 22:30:48 +0200
changeset 64157 3e4400f21310
parent 64156 01716e3c3e68
child 64158 2f7de0af23d3
tuned output;
src/Pure/Admin/isabelle_cronjob.scala
--- a/src/Pure/Admin/isabelle_cronjob.scala	Tue Oct 11 22:24:47 2016 +0200
+++ b/src/Pure/Admin/isabelle_cronjob.scala	Tue Oct 11 22:30:48 2016 +0200
@@ -28,7 +28,7 @@
     using(Mercurial.open_repository(root))(hg =>
       {
         hg.pull(options = "-q")
-        hg.identify("tip")
+        hg.identify("tip", options = "-i")
       })