From 4dc5fb5fc635774f73092fb86f98230bff7e17df Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Thu, 16 Jul 2015 11:44:46 +0200 Subject: [PATCH] small fix --- HOWTO.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/HOWTO.md b/HOWTO.md index 34e0cda3..d53f4f3b 100644 --- a/HOWTO.md +++ b/HOWTO.md @@ -6,7 +6,7 @@ 3. `make update_next_tag` (to update `@since` comments; be careful not to change symlinks) 4. update `CHANGELOG.md` (see its end to find the right git command) 5. commit the changes -6. `git checkout stable` +6. `git checkout stable; oasis setup` 7. `git merge master` 8. tag, and push both to github 9. new opam package