diff --git a/NEWS b/NEWS
index 819aa40c8..aab1407ec 100644
--- a/NEWS
+++ b/NEWS
@@ -1,4 +1,4 @@
-New in spot 2.8.7.dev (not yet released)
+New in spot 2.9 (2020-04-30)
 
   Command-line tools:
 
@@ -22,7 +22,7 @@ New in spot 2.8.7.dev (not yet released)
     select a range of their input formulas or automata (assuming a
     1-based numbering).
 
-  - When running translators ltlcross will now display {names} when
+  - When running translators, ltlcross will now display {names} when
     supplied.
 
   - ltlcross is now using the generic emptiness check procedure
@@ -96,8 +96,13 @@ New in spot 2.8.7.dev (not yet released)
     and the automaton is adjusted so that i also appears where j
     appeared.
 
+  - acc_code::unit_propagation() is a new method for performing unit
+    propagation in acceptance condition.  E.g.  Fin(0) | (Inf(0) &
+    Inf(1)) becomes Fin(0) | Inf(1).  This is now called by
+    simplify_acceptance_here().
+
   - propagate_marks_vector() and propagate_marks_here() are helper
-    functions for propagatings marks on the automaton: ignoring
+    functions for propagating marks on the automaton: ignoring
     self-loops and out-of-SCC transitions, marks common to all the
     input transitions of a state can be pushed to all its outgoing
     transitions, and vice-versa.  This is repeated until a fix point
@@ -112,20 +117,23 @@ New in spot 2.8.7.dev (not yet released)
     same transition structure (where the ..._maybe() variant would
     modify the Rabin automaton if needed).
 
-  - to_parity() has been rewritten now combines several strategies for
-    paritizing automata with any acceptance condition.
+  - to_parity() has been rewritten. It now combines several strategies
+    for paritizing automata with any acceptance condition.
 
   - relabel_bse(), used by ltlfilt --relabel-bool, is now better at
     dealing with n-ary operators and isolating subsets of operands
     that can be relabeled as a single term.
 
-  - print_dot() default was changed to use circles for automata with
+  - print_dot()'s default was changed to use circles for automata with
     fewer than 10 unamed states, ellipses for automata with up to 1000
     unamed states (or named states with up to 4 characters), and
     rounded rectangles otherwise.  Rectangles are also used for
     automata with acceptance bullets on states.  The new "E" option
     can be used to force rectangles in all situations.
 
+  - The generic emptiness check has been slightly improved (doing
+    fewer recursive calls in the worst case).
+
   Backward-incompatible changes:
 
   - iar() and iar_maybe() have been moved from
diff --git a/configure.ac b/configure.ac
index 98b8877f4..8b24ce007 100644
--- a/configure.ac
+++ b/configure.ac
@@ -21,7 +21,7 @@
 # along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
 AC_PREREQ([2.63])
-AC_INIT([spot], [2.8.7.dev], [spot@lrde.epita.fr])
+AC_INIT([spot], [2.9], [spot@lrde.epita.fr])
 AC_CONFIG_AUX_DIR([tools])
 AC_CONFIG_MACRO_DIR([m4])
 AM_INIT_AUTOMAKE([1.11 gnu tar-ustar color-tests parallel-tests])
diff --git a/doc/org/setup.org b/doc/org/setup.org
index 0527e117b..ad0283119 100644
--- a/doc/org/setup.org
+++ b/doc/org/setup.org
@@ -1,11 +1,11 @@
 #+OPTIONS: H:2 num:nil toc:t html-postamble:nil ^:nil
 #+EMAIL: spot@lrde.epita.fr
 #+HTML_LINK_HOME: index.html
-#+MACRO: SPOTVERSION 2.8.7
-#+MACRO: LASTRELEASE 2.8.7
-#+MACRO: LASTTARBALL [[http://www.lrde.epita.fr/dload/spot/spot-2.8.7.tar.gz][=spot-2.8.7.tar.gz=]]
-#+MACRO: LASTNEWS [[https://gitlab.lrde.epita.fr/spot/spot/blob/spot-2-8-7/NEWS][summary of the changes]]
-#+MACRO: LASTDATE 2020-03-13
+#+MACRO: SPOTVERSION 2.9
+#+MACRO: LASTRELEASE 2.9
+#+MACRO: LASTTARBALL [[http://www.lrde.epita.fr/dload/spot/spot-2.9.tar.gz][=spot-2.9.tar.gz=]]
+#+MACRO: LASTNEWS [[https://gitlab.lrde.epita.fr/spot/spot/blob/spot-2-9/NEWS][summary of the changes]]
+#+MACRO: LASTDATE 2020-04-30
 
 #+ATTR_HTML: :id spotlogo
 [[file:spot2.svg]]