diff --git a/sources b/sources
index 4fd5814..a66b83d 100644
--- a/sources
+++ b/sources
@@ -1,2 +1,2 @@
 SHA512 (why3-man.tar.xz) = 8355776ac8a67a56ae7354f8fd40dc5d2057022d1035090a3e38e139fbfe3c258fe3ccbed6e333cb005e66c7b4cdbbf6580e3420170fd08384cc9b36ce5ec2a1
-SHA512 (why3-1.3.1.tar.gz) = 2412c9bfcac8dbbee6657d39ec3ed006e1a8dc7522873041c53b9c572a752e7cc20b55378fe916e0f9d97de82705f6c01a17d2aa2f8c20a4fbdd2673bb78d34a
+SHA512 (why3-1.3.3.tar.gz) = a2dc95691cea29bbd20843a05add3985f777085086b654b53566ecdb752ba892366da703e232c85d5e0237d0e59564527aed55f6ccae9118d49e5f2cf93a53ce
diff --git a/why3.spec b/why3.spec
index 647003e..09c33e8 100644
--- a/why3.spec
+++ b/why3.spec
@@ -8,14 +8,14 @@
 %endif
 
 Name:           why3
-Version:        1.3.1
-Release:        14%{?dist}
+Version:        1.3.3
+Release:        4%{?dist}
 Summary:        Software verification platform
 
 # See LICENSE for the terms of the exception
 License:        LGPLv2 with exceptions
 URL:            http://why3.lri.fr/
-Source0:        https://gforge.inria.fr/frs/download.php/file/38291/%{name}-%{version}.tar.gz
+Source0:        https://gforge.inria.fr/frs/download.php/file/38367/%{name}-%{version}.tar.gz
 # Man pages written by Jerry James using text found in the sources.  Hence,
 # the copyright and license are the same as for the upstream sources.
 Source1:        %{name}-man.tar.xz
@@ -32,6 +32,7 @@ BuildRequires:  emacs-proofgeneral
 BuildRequires:  flocq
 BuildRequires:  latexmk
 BuildRequires:  libappstream-glib
+BuildRequires:  make
 BuildRequires:  ocaml
 BuildRequires:  ocaml-camlp5-devel
 BuildRequires:  ocaml-findlib
@@ -174,15 +175,6 @@ sed -e "s|-Wall|$RPM_OPT_FLAGS|;s/ -O -g//" \
 find -O3 examples -type f -perm /0111 -exec chmod a-x {} \+
 chmod a+x examples/*.sh
 
-# Remove spurious shebangs
-sed -i.orig '/#!.*/d' examples/use_api/runstrat/{echo,run}_wait.ml
-fixtimestamp examples/use_api/runstrat/echo_wait.ml
-fixtimestamp examples/use_api/runstrat/run_wait.ml
-
-# Fix end of line encodings
-sed -i.orig 's/\r//' examples/bts/20881.why
-fixtimestamp examples/bts/20881.why
-
 # Update the ProofGeneral integration instructions
 sed -i.orig 's,(MY_PATH_TO_WHY3)/share/whyitp,%{_emacs_sitelispdir},' share/whyitp/README
 fixtimestamp share/whyitp/README
@@ -194,8 +186,8 @@ make doc
 rm -f doc/html/.buildinfo examples/use_api/.merlin.in
 
 %install
-make install DESTDIR=%{buildroot}
-make install-lib DESTDIR=%{buildroot}
+%make_install
+make install-lib DESTDIR=%{?buildroot} INSTALL="%{__install} -p"
 
 %ifarch %{ocaml_native_compiler}
 # Install the native coq files
@@ -326,6 +318,21 @@ chmod 0755 %{buildroot}%{_bindir}/* \
 %files all
 
 %changelog
+* Sat Jan  2 2021 Jerry James <loganjerry@gmail.com> - 1.3.3-4
+- Rebuild for flocq 3.4.0
+
+* Wed Dec 23 2020 Jerry James <loganjerry@gmail.com> - 1.3.3-3
+- Rebuild for coq 8.12.2
+
+* Wed Dec  2 2020 Jerry James <loganjerry@gmail.com> - 1.3.3-2
+- Rebuild for coq 8.12.1 and menhir 20201201
+
+* Fri Sep 25 2020 Jerry James <loganjerry@gmail.com> - 1.3.3-1
+- Version 1.3.3
+
+* Thu Sep 03 2020 Richard W.M. Jones <rjones@redhat.com> - 1.3.1-14.1
+- Bump release and rebuild.
+
 * Wed Sep 02 2020 Richard W.M. Jones <rjones@redhat.com> - 1.3.1-14
 - OCaml 4.11.1 rebuild