diff options
| author | Alexey Dokuchaev <danfe@FreeBSD.org> | 2016-11-19 11:39:40 +0000 |
|---|---|---|
| committer | Alexey Dokuchaev <danfe@FreeBSD.org> | 2016-11-19 11:39:40 +0000 |
| commit | fa0784d10968fe99d5569385c7dda5214aa69cce (patch) | |
| tree | 49d84cbb83f7fb56ffce8ee0137f869557322d23 | |
| parent | Convert to USES=pyqt. (diff) | |
- Move license information from port description into LICENSE knobs
- Convert $arch-conditional BROKEN statement into BROKEN_$arch one
Notes
Notes:
svn path=/head/; revision=426358
| -rw-r--r-- | math/coq/Makefile | 18 | ||||
| -rw-r--r-- | math/coq/pkg-descr | 7 |
2 files changed, 10 insertions, 15 deletions
diff --git a/math/coq/Makefile b/math/coq/Makefile index cb37e341508d..2fe2b2efcf38 100644 --- a/math/coq/Makefile +++ b/math/coq/Makefile @@ -12,6 +12,9 @@ DISTNAME= ${PORTNAME}-${COQVERSION} MAINTAINER= johans@FreeBSD.org COMMENT= Theorem prover based on lambda-C +LICENSE= LGPL21 +LICENSE_FILE= ${WRKSRC}/LICENSE + BUILD_DEPENDS= camlp5:devel/ocaml-camlp5 \ ocamlfind:devel/ocaml-findlib @@ -27,12 +30,14 @@ CONFIGURE_ARGS= --prefix ${PREFIX} \ --opt MAKE_ENV= COQINSTALLPREFIX=${DESTDIR} +BROKEN_powerpc= does not link + OPTIONS_DEFINE= DOCS IDE OPTIONS_DEFAULT= IDE OPTIONS_SUB= yes IDE_DESC= Include desktop environment (coqide) IDE_BUILD_DEPENDS= lablgtk2:x11-toolkits/ocaml-lablgtk2 -IDE_RUN_DEPENDS:= lablgtk2:x11-toolkits/ocaml-lablgtk2 +IDE_RUN_DEPENDS= lablgtk2:x11-toolkits/ocaml-lablgtk2 IDE_CONFIGURE_OFF= --coqide no DOCS_USE= TEX=latex:build,dvipsk:build,texmf:build DOCS_BUILD_DEPENDS= hevea:textproc/hevea @@ -43,12 +48,6 @@ PORTDOCS= * add-plist-post: @${DO_NADA} -.include <bsd.port.pre.mk> - -.if ${ARCH} == "powerpc" -BROKEN= Does not link on powerpc -.endif - post-patch: @${REINPLACE_CMD} -e '/FreeBSD.*\.byte/s/^/#/' \ -e '1s:/bin/bash:/bin/sh:' \ @@ -57,6 +56,7 @@ post-patch: ${WRKSRC}/Makefile* ${WRKSRC}/install.sh @${REINPLACE_CMD} -e '/^#COQINSTALLPREFIX/{s/^#//;s|$$|$${DESTDIR}|;}' \ ${WRKSRC}/Makefile.build - @${REINPLACE_CMD} -e '/show_latex_mes/s/)$$/; true)/' ${WRKSRC}/Makefile.doc + @${REINPLACE_CMD} -e '/show_latex_mes/s/)$$/; true)/' \ + ${WRKSRC}/Makefile.doc -.include <bsd.port.post.mk> +.include <bsd.port.mk> diff --git a/math/coq/pkg-descr b/math/coq/pkg-descr index 597a3eeb9cb2..2557addcc410 100644 --- a/math/coq/pkg-descr +++ b/math/coq/pkg-descr @@ -1,5 +1,3 @@ -From the website: - Developed in the LogiCal project, the Coq tool is a formal proof management system: a proof done with Coq is mechanically checked by the machine. @@ -14,9 +12,6 @@ Coq is based on a logical framework called "Calculus of Inductive Constructions" extended by a modular development system for theories. -Coq is distributed under the GNU Lesser General Public Licence -Version 2.1 (LGPL). - CoqIde is installed if the x11-toolkits/ocaml-lablgtk2 port is installed. -WWW: http://coq.inria.fr/ +WWW: http://coq.inria.fr/ |