[!58] Hide repository credentials

Merge branch 'hide-repo-credentials' into 'master'

Closes: [#19]

See merge request [joe/pacxx-docker!58]

  [#19]: gitlab.dune-project.org/joe/pacxx-docker/issues/19
  [joe/pacxx-docker!58]: gitlab.dune-project.org/joe/pacxx-docker/merge_requests/58


Closes #19

base/verbose-git-status

@@ -6,6 +6,8 @@ dir=${1:?Need a directory to report status for}
 name=${2:?Need a project name to report}
 
 remote=$(git -C "$dir" remote get-url origin)
+# hide any credentials from the git url
+remote=$(printf '%s\n' "$remote" | sed 's,://[^/]*@,://,')
 branch=$(git -C "$dir" symbolic-ref -q --short HEAD)
 commit=$(git -C "$dir" rev-parse HEAD)