# HG changeset patch
# User wenzelm
# Date 1476217848 -7200
# Node ID 3e4400f21310a1bc62882ac12d336c40f8cd143f
# Parent  01716e3c3e68b8ea5c6a37d4bb54de622206e3df
tuned output;

diff -r 01716e3c3e68 -r 3e4400f21310 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")
       })