From 278fc02f3f43705d7f0e333e6d4ece3860ccc73d Mon Sep 17 00:00:00 2001
From: Erik Schnetter <schnetter@gmail.com>
Date: Mon, 25 Jul 2016 12:36:31 -0400
Subject: [PATCH] Don't require a `.git` suffix for the master repository name
 (#17606)

Closes #13881.
---
 base/version_git.sh | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/base/version_git.sh b/base/version_git.sh
index 38699a59092ee..8002fef21b34c 100644
--- a/base/version_git.sh
+++ b/base/version_git.sh
@@ -26,7 +26,7 @@ if [  "$#" = "2"  -a "$2" = "NO_GIT" ]; then
     exit 0
 fi
 # Collect temporary variables
-origin=$(git config -l 2>/dev/null | grep 'remote\.\w*\.url.*JuliaLang/julia.git' | sed -n 's/remote\.\([a-zA-Z]*\)\..*/\1\//p')
+origin=$(git config -l 2>/dev/null | grep 'remote\.\w*\.url.*JuliaLang/julia' | sed -n 's/remote\.\([a-zA-Z]*\)\..*/\1\//p')
 if [ -z "$origin" ]; then
     origin="origin/"
 fi