[Lunar-commits] <moonbase-other> coq: fix build with lablgtk & docs

v4hn me at v4hn.de
Sat Oct 13 13:37:01 CEST 2012


commit 0079111484fe5c31f5c1462bf74db012b1cfe561
Author: v4hn <me at v4hn.de>
Date: Sat, 13 Oct 2012 04:37:01 -0700
URL: https://github.com/lunar-linux/moonbase-other/commit/0079111484fe5c31f5c1462bf74db012b1cfe561

coq: fix build with lablgtk & docs
---
  compilers/coq/BUILD   | +3/-1     
  compilers/coq/DEPENDS | +2/-1     
  compilers/coq/DETAILS | +4/-0     
  3 files changed, 9 insertions(+), 2 deletions(-)

--- a/compilers/coq/BUILD
+++ b/compilers/coq/BUILD
@@ -1,6 +1,8 @@
 (
 
- ./configure -prefix /usr $OPTS &&
+ patch_it $SOURCE2 1 &&
+
+ ./configure -prefix /usr -configdir /etc $OPTS &&
  make world      &&
  prepare_install &&
  make install
--- a/compilers/coq/DEPENDS
+++ b/compilers/coq/DEPENDS
@@ -1,4 +1,5 @@
 depends ocaml
 depends camlp5
 
-optional_depends lablgtk "-coqide opt" "-coqide no" "to build a GTK IDE"
+optional_depends lablgtk "-coqide opt" "-coqide no" "build the GTK IDE"
+optional_depends hevea   "-with-doc yes" "-with-doc no" "build documentation"
--- a/compilers/coq/DETAILS
+++ b/compilers/coq/DETAILS
@@ -1,12 +1,16 @@
           MODULE=coq
          VERSION=8.4
           SOURCE=$MODULE-$VERSION.tar.gz
+         SOURCE2=$MODULE-lablgtk216.patch
       SOURCE_URL=http://coq.inria.fr/distrib/V${VERSION}/files/
+     SOURCE2_URL=$PATCH_URL
       SOURCE_VFY=sha1:2987aa418dd96a0df7284afe296293cb28814ef5
+     SOURCE2_VFY=sha1:d292e02ee556e7bd4e271c616619b697495015dc
         WEB_SITE=http://coq.inria.fr/
          ENTERED=20110829
          UPDATED=20121013
            SHORT="COQ is an interactive proof assistant"
+
 cat << EOF
 COQ is a Proof Assistant for a Logical Framework known as the Calculus of
 Inductive Constructions. It allows the interactive construction of formal




More information about the Lunar-commits mailing list