# HG changeset patch # User wenzelm # Date 1616861595 -3600 # Node ID 0e880b793db1d2a134575d738477673cfd77e708 # Parent 6e20976d58f5e94a8b7592865207716ad00612bb support repository archives (without full .hg directory); diff -r 6e20976d58f5 -r 0e880b793db1 NEWS --- a/NEWS Sat Mar 27 17:05:36 2021 +0100 +++ b/NEWS Sat Mar 27 17:13:15 2021 +0100 @@ -141,6 +141,12 @@ - Isabelle_System.download +*** System *** + +* Command-line tool "isabelle version" supports repository archives +(without full .hg directory). + + New in Isabelle2021 (February 2021) ----------------------------------- diff -r 6e20976d58f5 -r 0e880b793db1 lib/Tools/version --- a/lib/Tools/version Sat Mar 27 17:05:36 2021 +0100 +++ b/lib/Tools/version Sat Mar 27 17:13:15 2021 +0100 @@ -59,8 +59,12 @@ if [ -n "$SHORT_ID" ]; then if [ -n "$ISABELLE_ID" ]; then echo "$ISABELLE_ID" + elif [ -d "$ISABELLE_HOME/.hg" ]; then + "${HG:-hg}" -R "$ISABELLE_HOME" log -r "p1()" --template="{node|short}\n" 2>/dev/null || echo undefined + elif [ -f "$ISABELLE_HOME/.hg_archival.txt" ]; then + fgrep node: < "$ISABELLE_HOME/.hg_archival.txt" | cut -d " " -f2 | head -c12 else - "${HG:-hg}" -R "$ISABELLE_HOME" log -r "p1()" --template="{node|short}\n" 2>/dev/null || echo undefined + echo undefined fi else echo 'repository version' # filled in automatically! diff -r 6e20976d58f5 -r 0e880b793db1 src/Doc/System/Misc.thy --- a/src/Doc/System/Misc.thy Sat Mar 27 17:05:36 2021 +0100 +++ b/src/Doc/System/Misc.thy Sat Mar 27 17:13:15 2021 +0100 @@ -375,7 +375,9 @@ distribution, e.g.\ ``\<^verbatim>\Isabelle2021: February 2021\. The \<^verbatim>\-i\ option produces a short identification derived from the Mercurial - id of the @{setting ISABELLE_HOME} directory. + id of the @{setting ISABELLE_HOME} directory. This requires either a + repository clone or a repository archive (e.g. download of + \<^url>\https://isabelle.sketis.net/repos/isabelle/archive/tip.tar.gz\). \ end