Admin/churn
author blanchet
Tue, 01 Jun 2010 14:54:35 +0200
changeset 37261 c0fe8fa35771
parent 29556 7c128276aa93
child 40512 151fef652324
permissions -rwxr-xr-x
don't show spurious "..." in Nitpick's output for free variables of set type (e.g., P (op +) example from Manual_Nits.thy); undoes parts of 38ba15040455, which was too aggressive
     1 #!/bin/bash
     2 
     3 ADMIN="$(cd "$(dirname "$0")"; cd "$(pwd -P)"; pwd)"
     4 cd "$ADMIN"
     5 hg churn --aliases user-aliases --progress