Use HEAD instead of @ shortcut for git in launcher (#428)

The abbreviation @ for HEAD was added in git 1.8.5. The launcher claims to be compatible with git version 1.8.0 but the use of this abbreviation breaks this compatibility. This change is needed to support RHEL 7.6 which has only git 1.8.3.1.

diff --git a/launcher b/launcher
index 4e615927503187c33d970fc27142d7ad0238e080..39928d9f51ba2fabe735583c46259b98095a54a0 100755 (executable)
--- a/launcher
+++ b/launcher
@@ -760,9 +760,9 @@ case "$command" in
 
         git remote update
 
-        LOCAL=$(git rev-parse @)
+        LOCAL=$(git rev-parse HEAD)
         REMOTE=$(git rev-parse @{u})
-        BASE=$(git merge-base @ @{u})
+        BASE=$(git merge-base HEAD @{u})
 
         if [ $LOCAL = $REMOTE ]; then
           echo "Launcher is up-to-date"