diff --git a/sources b/sources
index a6db16b..4f8ade4 100644
--- a/sources
+++ b/sources
@@ -1,2 +1,2 @@
 SHA512 (why3-man.tar.xz) = 8355776ac8a67a56ae7354f8fd40dc5d2057022d1035090a3e38e139fbfe3c258fe3ccbed6e333cb005e66c7b4cdbbf6580e3420170fd08384cc9b36ce5ec2a1
-SHA512 (why3-1.2.0.tar.gz) = bc7dd11ef0ac80a86de9944bf4691011c6aa5f211280cbc7740ef6cfbf77657dd87106bc3197e41e404d808014bbff8fed2d209dc70deeca4566ade69cf33b5d
+SHA512 (why3-1.2.1.tar.gz) = 7a5d4403bda5a9c88490d83803a6c3d30b80b9949398de6d35b92df80a90980235c014d59afb46dd1bdd3028f20252ae1f59756a3d6978228e5c8fd9aefa1b3d
diff --git a/why3.appdata.xml b/why3.appdata.xml
new file mode 100644
index 0000000..d8aa5cc
--- /dev/null
+++ b/why3.appdata.xml
@@ -0,0 +1,43 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<component type="desktop">
+ <id>why3.desktop</id>
+ <metadata_license>0BSD</metadata_license>
+ <project_license>LGPL-2.1-only WITH OCaml-LGPL-linking-exception</project_license>
+ <name>Why3</name>
+ <summary>Software verification platform</summary>
+ <description>
+  <p>
+   Why3 is the next generation of the Why software verification platform.  Why3
+   clearly separates the purely logical specification part from generation of
+   verification conditions for programs.  It features a rich library of proof
+   task transformations that can be chained to produce a suitable input for a
+   large set of theorem provers, including SMT solvers, TPTP provers, as well as
+   interactive proof assistants.
+  </p>
+ </description>
+ <screenshots>
+  <screenshot type="default">
+   <image>http://why3.lri.fr/doc/gui-1.png</image>
+   <caption>Initial Why3 GUI window</caption>
+  </screenshot>
+  <screenshot>
+   <image>http://why3.lri.fr/doc/gui-2.png</image>
+   <image>The Why3 GUI with goal G1 selected</image>
+  </screenshot>
+  <screenshot>
+   <image>http://why3.lri.fr/doc/gui-3.png</image>
+   <image>The Why3 GUI after running Alt-Ergo on each goal</image>
+  </screenshot>
+  <screenshot>
+   <image>http://why3.lri.fr/doc/gui-4.png</image>
+   <image>The Why3 GUI after splitting goal G2</image>
+  </screenshot>
+  <screenshot>
+   <image>http://why3.lri.fr/doc/gui-5.png</image>
+   <image>File reloaded after modifying	 goal G2</image>
+  </screenshot>
+ </screenshots>
+ <updatecontact>loganjerry@gmail.com</updatecontact>
+ <url type="homepage">http://why3.lri.fr/</url>
+ <url type="bugtracker">https://gitlab.inria.fr/why3/why3/issues</url>
+</component>
diff --git a/why3.desktop b/why3.desktop
new file mode 100644
index 0000000..3e4a5fc
--- /dev/null
+++ b/why3.desktop
@@ -0,0 +1,9 @@
+[Desktop Entry]
+Name=Why3
+GenericName=Software Verifier
+Comment=Software verification platform
+Exec=why3 ide %f
+Icon=why3
+Type=Application
+Terminal=false
+Categories=Development;
diff --git a/why3.rpmlintrc b/why3.rpmlintrc
new file mode 100644
index 0000000..7b0f672
--- /dev/null
+++ b/why3.rpmlintrc
@@ -0,0 +1,28 @@
+# THIS FILE IS FOR WHITELISTING RPMLINT ERRORS AND WARNINGS IN TASKOTRON
+# https://fedoraproject.org/wiki/Taskotron/Tasks/dist.rpmlint#Whitelisting_errors
+
+# The dictionary lacks some technical words
+addFilter(r'W: spelling-error .* provers')
+
+# Caused by ocaml; this package cannot fix it
+addFilter(r'why3\.[^:]+: E: missing-call-to-chdir-with-chroot')
+
+# Indeed there is no documentation
+addFilter(r'ocaml-why3(|-devel).[^:]+: W: no-documentation')
+addFilter(r'why3-(all|emacs|xemacs).[^:]+: W: no-documentation')
+
+# This file is not a text file
+addFilter(r'W: file-not-utf8 .*\.mlw')
+
+# The TeX input carries its own character encoding declaration
+addFilter(r'why3-examples\.noarch: W: file-not-utf8 .*digit_sum\.tex')
+
+# The .notempty files are markers
+addFilter(r'why3-examples\.noarch: W: hidden-file-or-dir .*/\.notempty')
+addFilter(r'why3-examples\.noarch: E: zero-length .*/\.notempty')
+
+# We use the version of jquery provided by ocamldoc
+addFilter(r'W: unversioned-explicit-provides bundled\(jquery\)')
+
+# The man pages were created by the Fedora packager; there is no URL
+addFilter(r'why3\.spec: W: invalid-url Source1: why3-man\.tar\.xz')
diff --git a/why3.spec b/why3.spec
index 153a110..4900984 100644
--- a/why3.spec
+++ b/why3.spec
@@ -8,23 +8,28 @@
 %endif
 
 Name:           why3
-Version:        1.2.0
-Release:        6%{?dist}
+Version:        1.2.1
+Release:        1%{?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/37903/%{name}-%{version}.tar.gz
+Source0:        https://gforge.inria.fr/frs/download.php/file/38185/%{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
+# Desktop file written by Jerry James
+Source2:        %{name}.desktop
+# AppData file written by Jerry James
+Source3:        %{name}.appdata.xml
 
 BuildRequires:  coq
+BuildRequires:  emacs-proofgeneral
 BuildRequires:  evince
 BuildRequires:  flocq
-BuildRequires:  gtksourceview2-devel
 BuildRequires:  hevea
+BuildRequires:  libappstream-glib
 BuildRequires:  ocaml
 BuildRequires:  ocaml-camlp5-devel
 BuildRequires:  ocaml-findlib
@@ -36,6 +41,7 @@ BuildRequires:  ocaml-num-devel
 BuildRequires:  ocaml-sqlite-devel
 BuildRequires:  ocaml-zarith-devel
 BuildRequires:  ocaml-zip-devel
+BuildRequires:  pkgconfig(gtksourceview-2.0)
 BuildRequires:  rubber
 BuildRequires:  tex(comment.sty)
 BuildRequires:  tex(upquote.sty)
@@ -43,6 +49,7 @@ BuildRequires:  tex-urlbst
 BuildRequires:  emacs xemacs xemacs-packages-extra
 
 Requires:       gtksourceview2
+Requires:       hicolor-icon-theme
 Requires:       texlive-base
 Requires:       vim-filesystem
 Provides:       bundled(jquery)
@@ -111,6 +118,15 @@ Requires:       ocaml-zip-devel%{?_isa}
 This package contains development files needed to build applications
 that use the ocaml-%{name} library.
 
+%package proofgeneral
+Summary:        Why3 integration with ProofGeneral
+Requires:       %{name} = %{version}-%{release}
+Requires:       emacs-proofgeneral
+BuildArch:      noarch
+
+%description proofgeneral
+This package provides a why3 plugin for ProofGeneral.
+
 %prep
 %setup -q
 %setup -q -T -D -a 1
@@ -124,13 +140,14 @@ fixtimestamp() {
 # network use
 # Link the binaries with runtime compiled with -fPIC.
 # This avoids many link-time errors.
-sed -e "s|-Wall|$RPM_OPT_FLAGS|" \
+sed -e "s|-Wall|$RPM_OPT_FLAGS|;s/ -O -g//" \
     -e "s/cp /cp -p /" \
     -e "s|^OLINKFLAGS =.*|& -runtime-variant _pic -ccopt \"$RPM_LD_FLAGS\"|" \
     -i Makefile.in
 
 # Remove spurious executable bits
 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
@@ -141,6 +158,10 @@ fixtimestamp examples/use_api/runstrat/run_wait.ml
 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
+
 %build
 %configure --enable-verbose-make
 make #%%{?_smp_mflags}
@@ -176,20 +197,35 @@ mkdir -p %{buildroot}%{_datadir}/gtksourceview-2.0
 mv %{buildroot}%{_datadir}/%{name}/lang \
    %{buildroot}%{_datadir}/gtksourceview-2.0/language-specs
 
+# Install the desktop file
+mkdir -p %{buildroot}%{_datadir}/applications
+desktop-file-install --dir=%{buildroot}%{_datadir}/applications %{SOURCE2}
+
+# Install the icon
+mkdir -p %{buildroot}%{_datadir}/icons/hicolor/scalable
+cp -p share/images/src/logo-kim.svg \
+      %{buildroot}%{_datadir}/icons/hicolor/scalable/%{name}.svg
+
+# Install the AppStream metadata
+mkdir -p %{buildroot}%{_metainfodir}
+cp -p %{SOURCE3} %{buildroot}%{_metainfodir}
+appstream-util validate-relax --nonet %{buildroot}%{_metainfodir}/%{name}.appdata.xml
+
 # Move the vim file to the right place
 mkdir -p %{buildroot}%{_datadir}/vim/vimfiles
 mv %{buildroot}%{_datadir}/%{name}/vim/ftdetect \
    %{buildroot}%{_datadir}/%{name}/vim/syntax \
    %{buildroot}%{_datadir}/vim/vimfiles
 
-# Byte compile the (X)Emacs support file
+# Byte compile the (X)Emacs support files
 mkdir -p %{buildroot}%{_xemacs_sitelispdir}
 cp -p %{buildroot}%{_emacs_sitelispdir}/%{name}.el \
    %{buildroot}%{_xemacs_sitelispdir}
+cp -p share/whyitp/whyitp.el %{buildroot}%{_emacs_sitelispdir}
 pushd %{buildroot}%{_xemacs_sitelispdir}
 %{_xemacs_bytecompile} %{name}.el
 cd %{buildroot}%{_emacs_sitelispdir}
-%{_emacs_bytecompile} %{name}.el
+%{_emacs_bytecompile} %{name}.el whyitp.el
 popd
 
 # Remove misplaced documentation
@@ -206,14 +242,17 @@ chmod 0755 %{buildroot}%{_bindir}/* \
 %license LICENSE
 %{_bindir}/%{name}
 %{_datadir}/%{name}/
+%{_datadir}/applications/%{name}.desktop
 %{_datadir}/bash-completion/
 %{_datadir}/gtksourceview-2.0/language-specs/%{name}.lang
+%{_datadir}/icons/hicolor/scalable/%{name}.svg
 %{_datadir}/vim/vimfiles/ftdetect/%{name}.vim
 %{_datadir}/vim/vimfiles/syntax/%{name}.vim
 %{_datadir}/zsh/
 %{_texmf}/tex/latex/why3/
 %{_libdir}/%{name}/
 %{_mandir}/man1/%{name}*
+%{_metainfodir}/%{name}.appdata.xml
 
 %files -n ocaml-%{name}
 %dir %{_libdir}/ocaml/%{name}/
@@ -241,11 +280,20 @@ chmod 0755 %{buildroot}%{_bindir}/* \
 %files xemacs
 %{_xemacs_sitelispdir}/%{name}.el*
 
+%files proofgeneral
+%doc share/whyitp/README
+%{_emacs_sitelispdir}/whyitp.el*
+
 # "why3-all" is a meta-package; it just depends on other packages, so that
 # it's easier to install a useful suite of tools.  Thus, it has no files:
 %files all
 
 %changelog
+* Tue Oct 29 2019 Jerry James <loganjerry@gmail.com> - 1.2.1-1
+- New upstream release
+- Add -proofgeneral subpackage
+- Add desktop and AppData files
+
 * Fri Oct 11 2019 Jerry James <loganjerry@gmail.com> - 1.2.0-6
 - Rebuild for ocaml-menhir 20190924