From 37ac602d7224b92bcbf2c4c5c4535cbb7dfe599e Mon Sep 17 00:00:00 2001
From: Mike Gerber <mike.gerber@sbb.spk-berlin.de>
Date: Wed, 23 Feb 2022 14:33:37 +0100
Subject: [PATCH] git push

---
 README-DEV.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/README-DEV.md b/README-DEV.md
index e490f49..55c0ffd 100644
--- a/README-DEV.md
+++ b/README-DEV.md
@@ -13,7 +13,7 @@ Releasing
 * Update `ocrd-tool.json` version (the `setup.py` version is read from this)
 * `git commit -m 'v<version>'`
 * `git tag -m 'v<version>' 'v<version>'`
-* `git push --tags`
+* `git push; git push --tags`
 * Do a release on GitHub
 
 ### Uploading to PyPI