From f974abc9ef7bf3cf0076136d8bacb7f6cc0120e3 Mon Sep 17 00:00:00 2001 From: Dominik Jain Date: Sat, 11 Apr 2026 15:29:20 +0200 Subject: [PATCH] Improve release process description --- README-dev.md | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/README-dev.md b/README-dev.md index 958e4893..cd5fce8f 100644 --- a/README-dev.md +++ b/README-dev.md @@ -16,4 +16,5 @@ and tools for formatting and type checking. This also creates the git tag. 3. Push to GitHub, triggering the release process. - git push --tags \ No newline at end of file + git push + git push --tags