diff --git a/RELEASE.md b/RELEASE.md index 5e66ffee0c..185e893c15 100644 --- a/RELEASE.md +++ b/RELEASE.md @@ -146,6 +146,8 @@ tags and re-perform the required release steps: ```sh ; git tag -d X.Y.Z # Erase git tag locally ; git push -d upstream X.Y.Z # Erase git tag on GitHib + +; dune-release tag # Re-create tag ; dune-release distrib --skip-tests ; dune-release publish distrib --verbose ; dune-release publish doc --verbose # ... if necessary