auxprogs/make_or_upd_vgversion_h : accept a git worktree as a git dir

A directory can be a git directory in 2 cases:
  * it is a git repository, checked with -d .git
  + it is a git worktree directory (see git help worktree)

Modify auxprogs/make_or_upd_vgversion_h so that it detects worktree directory
and produces a correct git version for --version -v

diff --git a/auxprogs/make_or_upd_vgversion_h b/auxprogs/make_or_upd_vgversion_h
index 7787b4c1ee6866b09170ce9b912891440722cafe..ea6f068989fcc848857f7ffd691eb06ec6aefb95 100755 (executable)
--- a/auxprogs/make_or_upd_vgversion_h
+++ b/auxprogs/make_or_upd_vgversion_h
@@ -2,7 +2,9 @@
 
 extract_git_version()
 {
-    if [ -d "$1"/.git ]
+    PREVPWD="$PWD"
+    cd "$1"
+    if [ -d ./.git ] || git rev-parse --is-inside-work-tree > /dev/null 2> /dev/null
     then
         REV=$(git show --format=%H#%ci -s $(git rev-parse HEAD) |
                      sed -e 's/ .*//' -e 's/[0-9a-f]\{30\}#/#/' -e 's/-//g' \
@@ -11,7 +13,8 @@ extract_git_version()
         echo $REV$X
     else
         echo "unknown"
-    fi    
+    fi
+    cd "$PREVPWD"
 }
 
 srcdir="${1:-.}"
@@ -24,7 +27,7 @@ else
 /* Do not edit: file generated by auxprogs/make_or_upd_vgversion_h.
    This file defines VGGIT, used to report GIT revision
    when using command line options:  -v --version
-   The produced VGGIT format is 
+   The produced VGGIT format is
       hhhhhhhhhh-YYYYMMDDX
    where hhhhhhhhhh is the first 10 characters of the HEAD commit
          YYYYMMDD is the commit date