Bug fix: checkout $TAG.

2019-08-15 15:53:42 +01:00 · 2019-08-15 15:53:42 +01:00 · ff0a40b62a
parent 6b1864e677
commit ff0a40b62a
1 changed files with 1 additions and 1 deletions
--- a/.ci/mk_release
+++ b/.ci/mk_release
@ -75,7 +75,7 @@ clone_repo()
    git clone . $ISADOF_DIR
    if [ "$USE_TAG" = "true" ]; then
        echo "  * Switching to tag $DOF_VERSION/$ISABELLE_SHORT_VERSION"
-        (cd $ISADOF_DIR && git checkout $DOF_VERSION/$ISABELLE_SHORT_VERSION)
+        (cd $ISADOF_DIR && git checkout $TAG)
    else
        echo "  * Not tag specified, using master branch"
    fi