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