[why/f21] Rebuild for flocq 2.4.0 and why3 0.84. Fix license handling. BR emacs instead of emacs-nox.

[Jerry James]

commit dcfb5e236969d54c55ef3fd28f176353d12cb3a5
Author: Jerry James <jamesjer at betterlinux.com>
Date:   Mon Sep 8 14:11:02 2014 -0600

    Rebuild for flocq 2.4.0 and why3 0.84.
    Fix license handling.
    BR emacs instead of emacs-nox.

 why-flocq23.patch |   11 -----------
 why-flocq24.patch |   14 ++++++++++++++
 why.spec          |   19 ++++++++++++++-----
 3 files changed, 28 insertions(+), 16 deletions(-)
---
diff --git a/why-flocq24.patch b/why-flocq24.patch
new file mode 100644
index 0000000..e4f10a4
--- /dev/null
+++ b/why-flocq24.patch
@@ -0,0 +1,14 @@
+--- ./lib/coq/WhyFloats.v.orig	2014-03-17 16:01:46.000000000 -0600
++++ ./lib/coq/WhyFloats.v	2014-09-02 17:40:03.356028320 -0600
+@@ -106,9 +106,9 @@ apply Zlt_succ_le.
+ change (Zpos m < Zsucc (Zpred (Zpower_pos 2 prec)))%Z.
+ rewrite <- Zsucc_pred.
+ generalize (Zeq_bool_eq _ _ H1). clear.
+-rewrite Fcalc_digits.Z_of_nat_S_digits2_Pnat.
++rewrite Fcore_digits.Zpos_digits2_pos.
+ intros H.
+-apply (Fcalc_digits.Zpower_gt_Zdigits Fcalc_digits.radix2 (Zpos prec) (Zpos m)).
++apply (Fcore_digits.Zpower_gt_Zdigits Fcore_Zaux.radix2 (Zpos prec) (Zpos m)).
+ revert H.
+ unfold FLT_exp.
+ generalize (Fcore_digits.Zdigits radix2 (Zpos m)).
diff --git a/why.spec b/why.spec
index 17c8393..8c9f6b4 100644
--- a/why.spec
+++ b/why.spec
@@ -10,7 +10,7 @@
 
 Name:           why
 Version:        2.34
-Release:        8%{?dist}
+Release:        9%{?dist}
 Summary:        Software verification platform
 
 License:        LGPLv2 with exceptions
@@ -47,8 +47,8 @@ Patch0:         gwhy-2.33.patch
 # this case.
 Patch1:         %{name}-2.34-Makefile.in.patch
 
-# Adapt to flocq 2.3.0
-Patch2:         %{name}-flocq23.patch
+# Adapt to flocq 2.4.0
+Patch2:         %{name}-flocq24.patch
 
 # Avoid a clash between Frama-C and why modules both named "Project".
 # Sent upstream 26 Jun 2014.
@@ -57,7 +57,7 @@ Patch3:         %{name}-project.patch
 BuildRequires:  auto-destdir
 BuildRequires:  cvc3
 BuildRequires:  desktop-file-utils
-BuildRequires:  emacs-nox xemacs xemacs-packages-extra
+BuildRequires:  emacs xemacs xemacs-packages-extra
 BuildRequires:  frama-c-devel
 BuildRequires:  gappalib-coq
 BuildRequires:  gtk2-devel
@@ -260,6 +260,9 @@ sed -e 's/command = "pvs"/command = "pvs-sbcl"/' \
     -i tools/dpConfig.ml
 sed -i 's/pvs/pvs-sbcl/' configure
 
+# Build with why3 0.84
+sed -i 's/0\.83/0.84/' configure
+
 %build
 %if ! %{opt}
 %global opt_option OCAMLBEST=byte OCAMLC=ocamlc OCAMLDEP=ocamldep OCAMLYACC=ocamlyacc OCAMLLEX=ocamllex
@@ -311,7 +314,7 @@ cp -p %{SOURCE12}             %{buildroot}%{_bindir}/
 mkdir -p %{buildroot}%{why_examples_dir}mlw/
 mkdir -p %{buildroot}%{why_examples_dir}c/
 cp -p doc/manual.ps %{buildroot}%{why_doc_dir}/why-manual.ps
-cp -p %{SOURCE8} %{SOURCE3} CHANGES COPYING LICENSE README Version %{buildroot}%{why_doc_dir}
+cp -p %{SOURCE8} %{SOURCE3} CHANGES README Version %{buildroot}%{why_doc_dir}
 
 # Copy in the example files, leaving behind all generated files
 cd examples
@@ -375,6 +378,7 @@ touch --no-create %{_datadir}/icons/hicolor &>/dev/null
 gtk-update-icon-cache %{_datadir}/icons/hicolor &>/dev/null || :
 
 %files
+%license COPYING LICENSE
 %{_bindir}/*
 %{_libdir}/why/
 %{_mandir}/man1/why.1*
@@ -432,6 +436,11 @@ gtk-update-icon-cache %{_datadir}/icons/hicolor &>/dev/null || :
 
 
 %changelog
+* Mon Sep  8 2014 Jerry James <loganjerry at gmail.com> - 2.34-9
+- Rebuild for flocq 2.4.0 and why3 0.84
+- Fix license handling
+- BR emacs instead of emacs-nox
+
 * Mon Aug 18 2014 Fedora Release Engineering <rel-eng at lists.fedoraproject.org> - 2.34-8
 - Rebuilt for https://fedoraproject.org/wiki/Fedora_21_22_Mass_Rebuild