| changeset 73523 | 2cd23d587db9 |
| parent 73521 | a6ca869af096 |
| 73522:b219774a71ae | 73523:2cd23d587db9 |
|---|---|
60 |
60 |
61 |
61 |
62 ## main |
62 ## main |
63 |
63 |
64 if [ -z "$SHORT_ID" -a -z "$TAGS" ]; then |
64 if [ -z "$SHORT_ID" -a -z "$TAGS" ]; then |
65 echo 'repository version' # filled in automatically! |
65 echo "$ISABELLE_NAME" |
66 fi |
66 fi |
67 |
67 |
68 HG_ARCHIVAL="$ISABELLE_HOME/.hg_archival.txt" |
68 HG_ARCHIVAL="$ISABELLE_HOME/.hg_archival.txt" |
69 |
69 |
70 export LANG=C |
70 export LANG=C |