etc/update_version.sh: deal with -DEV versions in CHANGES.md

oscar-system · Apr 21, 2022 · b67dcbc · b67dcbc
1 parent 9ffd1be
commit b67dcbc
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/etc/update_version.sh b/etc/update_version.sh
@@ -27,8 +27,8 @@ git diff-index --quiet HEAD -- || error "uncommitted changes detected"
 echo "Setting version to $relvers, released $reldate_iso"
 
 # check that CHANGES.md has correct entry
-if egrep -q "^## Version ${relvers} " CHANGES.md ; then
-    perl -pi -e "s;^## Version ${relvers} \([^)]+\)$;## Version ${relvers} (released ${reldate_iso});" CHANGES.md
+if egrep -q "^## Version ${relvers}(-DEV)? " CHANGES.md ; then
+    perl -pi -e "s;^## Version ${relvers}(-DEV)? \([^)]+\)$;## Version ${relvers} (released ${reldate_iso});" CHANGES.md
 elif [[ ${relvers} = *-DEV ]] ; then
     perl -pi -e "s;^(# Changes in GAP.jl)$;\1\n\n## Version ${relvers} (released YYYY-MM-DD);" CHANGES.md
 else