Revise release directory naming

Revise release directory naming

Include the Git tag in the name of the release directory rather than
just the version number.  Revise the script for the "release" job
accordingly.  This enables using the $CI_COMMIT_TAG variable in job
scripts without the need to resort to string manipulation to strip the
leading "v", improving readability.  The only place where string
manipulation is applied to the Git tag is now the "release" job itself,
to verify that the Git tag matches the version number embedded in the
source tarball name.

(cherry picked from commit 8d548cbb58492a929a5c520b03ae1eefce204dbb)