From d98dd0084a85a9c37c3ca923bcb1458622026b81 Mon Sep 17 00:00:00 2001
From: Diogo Sousa <diogogsousa@gmail.com>
Date: Sun, 5 Nov 2023 20:07:15 +0000
Subject: [PATCH] Release script is now more flexible about release notes.

---
 tools/release.sh | 13 +++++++------
 1 file changed, 7 insertions(+), 6 deletions(-)

diff --git a/tools/release.sh b/tools/release.sh
index 0932b4d..6459573 100755
--- a/tools/release.sh
+++ b/tools/release.sh
@@ -46,11 +46,6 @@ echo "Current version is $(project_version)."
 echo -n "Which version do you want to release? "
 read release_version
 
-if ! grep "^## " release-notes.md | head -1 | grep --silent "^## $release_version$"; then
-    echo "You forgot to update the release notes." >&2
-    exit 1
-fi
-
 echo -n "Which will be the next version? "
 read next_version
 
@@ -80,6 +75,12 @@ fi
 
 echo "done."
 
+while ! grep "^## " release-notes.md | head -1 | grep --silent "^## $release_version$"; do
+    echo "There's no entry for this version in the release notes."
+    echo -n "Go ahead and add them and press enter when you're done... "
+    read
+done
+
 set_version "$release_version"
 
 git commit -am "Release v${release_version}."
@@ -89,7 +90,7 @@ set_version "$next_version"
 
 git commit -am "Bump to version $next_version."
 
-echo "Check if everything is alright.  If so do:"
+echo "Check if everything is alright.  If so, open a PR, merge it, and then do:"
 echo
 echo "  git push --atomic origin $MAIN_BRANCH v${release_version} && git checkout v${release_version} && cargo publish && git checkout $MAIN_BRANCH"
 echo