# It does not affect GIT tags. Use this script immediately
# before making a release, to remove the "-dev" tag and to
# update the version label. Then commit the change and tag
# It does not affect GIT tags. Use this script immediately
# before making a release, to remove the "-dev" tag and to
# update the version label. Then commit the change and tag