improved get_git_version

2023-05-14 21:00:45 +02:00
1 parent fd25d0cf2e
commit feab44b34a
@@ -10,5 +10,6 @@ set head=`git rev-parse HEAD`
 echo -n $head
 echo -n ' dated '
 echo -n `git show -s --format=%ci $head`
+echo -n ' compiled on ' `date` 'at' `hostname` 'by' `whoami`
 echo -n '"'
 echo ';'