Index: head/math/coq/Makefile
===================================================================
--- head/math/coq/Makefile	(revision 426357)
+++ head/math/coq/Makefile	(revision 426358)
@@ -1,62 +1,62 @@
 # Created by: Rene Ladan <r.c.ladan@student.tue.nl>
 # $FreeBSD$
 
 PORTNAME=	coq
 PORTVERSION=	8.4.6
 PORTEPOCH=	2
 CATEGORIES=	math
 MASTER_SITES=	http://coq.inria.fr/distrib/V${COQVERSION}/files/ \
 		ftp://ftp.stack.nl/pub/users/johans/coq/
 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
 
 COQVERSION=	${PORTVERSION:R}pl${PORTVERSION:E}
 USES=		gmake
 USE_OCAML=	yes
 ALL_TARGET=	world
 
 HAS_CONFIGURE=	yes
 CONFIGURE_ARGS=	--prefix ${PREFIX} \
 		--mandir ${PREFIX}/man \
 		--emacslib ${PREFIX}/share/emacs/site-lisp \
 		--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
 DOCS_CONFIGURE_OFF=	--with-doc none
 PORTDOCS=		*
 
 # Workaround bsd.ocaml.mk to fix packaging
 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:' \
 		-e '/^MAKE=/d' ${WRKSRC}/configure
 	@${REINPLACE_CMD} -e 's:/bin/bash:/bin/sh:' \
 		${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>
Index: head/math/coq/pkg-descr
===================================================================
--- head/math/coq/pkg-descr	(revision 426357)
+++ head/math/coq/pkg-descr	(revision 426358)
@@ -1,22 +1,17 @@
-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.
 
 In particular, Coq allows:
 * the definition of functions or predicates,
 * to state mathematical theorems and software specifications,
 * to develop interactively formal proofs of these theorems,
 * to check these proofs by a small certification "kernel".
 
 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/