From owner-svn-ports-head@freebsd.org Sat Nov 19 11:39:41 2016 Return-Path: Delivered-To: svn-ports-head@mailman.ysv.freebsd.org Received: from mx1.freebsd.org (mx1.freebsd.org [IPv6:2001:1900:2254:206a::19:1]) by mailman.ysv.freebsd.org (Postfix) with ESMTP id 90B76C49669; Sat, 19 Nov 2016 11:39:41 +0000 (UTC) (envelope-from danfe@FreeBSD.org) Received: from repo.freebsd.org (repo.freebsd.org [IPv6:2610:1c1:1:6068::e6a:0]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (Client did not present a certificate) by mx1.freebsd.org (Postfix) with ESMTPS id 48C57108A; Sat, 19 Nov 2016 11:39:41 +0000 (UTC) (envelope-from danfe@FreeBSD.org) Received: from repo.freebsd.org ([127.0.1.37]) by repo.freebsd.org (8.15.2/8.15.2) with ESMTP id uAJBdeCg028324; Sat, 19 Nov 2016 11:39:40 GMT (envelope-from danfe@FreeBSD.org) Received: (from danfe@localhost) by repo.freebsd.org (8.15.2/8.15.2/Submit) id uAJBdeve028322; Sat, 19 Nov 2016 11:39:40 GMT (envelope-from danfe@FreeBSD.org) Message-Id: <201611191139.uAJBdeve028322@repo.freebsd.org> X-Authentication-Warning: repo.freebsd.org: danfe set sender to danfe@FreeBSD.org using -f From: Alexey Dokuchaev Date: Sat, 19 Nov 2016 11:39:40 +0000 (UTC) To: ports-committers@freebsd.org, svn-ports-all@freebsd.org, svn-ports-head@freebsd.org Subject: svn commit: r426358 - head/math/coq X-SVN-Group: ports-head MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit X-BeenThere: svn-ports-head@freebsd.org X-Mailman-Version: 2.1.23 Precedence: list List-Id: SVN commit messages for the ports tree for head List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: Sat, 19 Nov 2016 11:39:41 -0000 Author: danfe Date: Sat Nov 19 11:39:40 2016 New Revision: 426358 URL: https://svnweb.freebsd.org/changeset/ports/426358 Log: - Move license information from port description into LICENSE knobs - Convert $arch-conditional BROKEN statement into BROKEN_$arch one Modified: head/math/coq/Makefile head/math/coq/pkg-descr Modified: head/math/coq/Makefile ============================================================================== --- head/math/coq/Makefile Sat Nov 19 11:33:05 2016 (r426357) +++ head/math/coq/Makefile Sat Nov 19 11:39:40 2016 (r426358) @@ -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 - -.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 +.include Modified: head/math/coq/pkg-descr ============================================================================== --- head/math/coq/pkg-descr Sat Nov 19 11:33:05 2016 (r426357) +++ head/math/coq/pkg-descr Sat Nov 19 11:39:40 2016 (r426358) @@ -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 call 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/