[base] Remove verbose-git-status script.

This is no longer used and has been emitting deprecation messages for a while.

Closes: #31

base/Dockerfile

@@ -34,7 +34,7 @@ RUN set -ex;                                            \
 ENV CCACHE_DIR=/cache/ccache
 ENV PATH=/usr/lib/ccache:$PATH
 
-COPY --chown=root:root getpacxx verbose-git-status /usr/local/bin/
+COPY --chown=root:root getpacxx /usr/local/bin/
 
 RUN adduser --disabled-password --home /ci --uid 50000 --gecos "" ci
     

base/verbose-git-status

-#!/bin/sh
-
-echo >&2 "Warning: verbose-git-status is going away, see https://gitlab.dune-project.org/joe/pacxx-docker/issues/20"
-
-# verbose-git-status DIR NAME
-
-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)
-
-echo "Project $name in $dir: on branch ${branch:-(detached)} at $commit from $remote"