lib/Tools/version
author wenzelm
Tue Aug 11 15:53:13 2009 +0200 (2009-08-11)
changeset 32361 141e5151b918
parent 29143 72c960b2b83e
child 41511 2fe62d602681
permissions -rwxr-xr-x
clarified situation about unidentified repository versions -- in a distributed setting there is not "the" repository;
berghofe@13804
     1
#!/usr/bin/env bash
berghofe@13804
     2
#
berghofe@13804
     3
# Author: Stefan Berghofer, TU Muenchen
berghofe@13804
     4
#
berghofe@13804
     5
# DESCRIPTION: display Isabelle version
berghofe@13804
     6
wenzelm@32361
     7
echo 'unidentified repository version'    # filled in automatically!