[Pkg-ocaml-maint-commits] r2648 - in /trunk/packages/coq-doc:
branches/ branches/8.0pl3+8.1alpha/
branches/8.0pl3+8.1alpha/debian/ branches/8.0pl3+8.1alpha/debian/patches/
branches/upstream/ trunk/debian/
smimram at users.alioth.debian.org
smimram at users.alioth.debian.org
Fri Apr 28 18:21:08 UTC 2006
Author: smimram
Date: Fri Apr 28 18:21:01 2006
New Revision: 2648
URL: http://svn.debian.org/wsvn/pkg-ocaml-maint/?sc=1&rev=2648
Log:
Preparing the 8.1 upload.
Added:
trunk/packages/coq-doc/branches/
trunk/packages/coq-doc/branches/8.0pl3+8.1alpha/
- copied from r2334, trunk/packages/coq-doc/trunk/
trunk/packages/coq-doc/branches/8.0pl3+8.1alpha/debian/
- copied from r2335, trunk/packages/coq-doc/trunk/debian/
trunk/packages/coq-doc/branches/8.0pl3+8.1alpha/debian/Makefile.config
trunk/packages/coq-doc/branches/8.0pl3+8.1alpha/debian/patches/
trunk/packages/coq-doc/branches/8.0pl3+8.1alpha/debian/patches/00list
trunk/packages/coq-doc/branches/8.0pl3+8.1alpha/debian/patches/config_makefile.dpatch (with props)
trunk/packages/coq-doc/branches/upstream/
trunk/packages/coq-doc/branches/upstream/coq-doc_8.0pl3+8.1alpha.orig.tar.gz (with props)
Removed:
trunk/packages/coq-doc/branches/8.0pl3+8.1alpha/coq-doc_8.0pl1.0.orig.tar.gz
trunk/packages/coq-doc/branches/8.0pl3+8.1alpha/debian/coq-doc-html.doc-base.library
trunk/packages/coq-doc/branches/8.0pl3+8.1alpha/debian/dirs
trunk/packages/coq-doc/trunk/debian/coq-doc-html.doc-base.library
trunk/packages/coq-doc/trunk/debian/dirs
Modified:
trunk/packages/coq-doc/branches/8.0pl3+8.1alpha/debian/changelog
trunk/packages/coq-doc/branches/8.0pl3+8.1alpha/debian/control
trunk/packages/coq-doc/branches/8.0pl3+8.1alpha/debian/copyright
trunk/packages/coq-doc/branches/8.0pl3+8.1alpha/debian/rules
trunk/packages/coq-doc/trunk/debian/changelog
trunk/packages/coq-doc/trunk/debian/control
Added: trunk/packages/coq-doc/branches/8.0pl3+8.1alpha/debian/Makefile.config
URL: http://svn.debian.org/wsvn/pkg-ocaml-maint/trunk/packages/coq-doc/branches/8.0pl3%2B8.1alpha/debian/Makefile.config?rev=2648&op=file
==============================================================================
--- trunk/packages/coq-doc/branches/8.0pl3+8.1alpha/debian/Makefile.config (added)
+++ trunk/packages/coq-doc/branches/8.0pl3+8.1alpha/debian/Makefile.config Fri Apr 28 18:21:01 2006
@@ -1,0 +1,111 @@
+##################################
+#
+# Configuration file for Coq
+#
+##################################
+
+#############################################################################
+#
+# This file is generated by the script "configure"
+#
+# DO NOT EDIT IT !! DO NOT EDIT IT !! DO NOT EDIT IT !! DO NOT EDIT IT !!
+#
+# If something is wrong below, then rerun the script "configure"
+# with the good options (see the file INSTALL).
+#
+#############################################################################
+
+# Local use (no installation)
+LOCAL=false
+
+# Paths for true installation
+# BINDIR=path where coqtop, coqc, coqmktop, coq-tex, coqdep, gallina and
+# do_Makefile will reside
+# LIBDIR=path where the Coq library will reside
+# MANDIR=path where to install manual pages
+# EMACSDIR=path where to put Coq's Emacs mode (coq.el)
+BINDIR="/usr/bin"
+COQLIB="/usr/lib/coq"
+MANDIR="/usr/share/man"
+EMACSLIB="/usr/share/emacs/site-lisp/coq"
+EMACS=
+
+# Path to Coq distribution
+COQTOP=/usr
+VERSION=8.1-alpha
+
+# Directory containing Camlp4 binaries. Can be empty if camlp4 is in the PATH
+CAMLP4BIN=/usr/bin
+
+# Ocaml version number
+CAMLVERSION=OCAML309
+
+# Ocaml .h directory
+CAMLHLIB=/usr/lib/ocaml/3.09.1/caml
+
+# Camlp4 library directory (avoid CAMLP4LIB used on Windows)
+CAMLP4O=camlp4o
+CAMLP4COMPAT=-loc loc
+MYCAMLP4LIB=+camlp4
+
+# Objective-Caml compile command
+OCAMLC=ocamlc.opt
+OCAMLOPT=ocamlopt.opt
+
+# Caml link command and Caml make top command
+CAMLLINK=ocamlc.opt
+CAMLOPTLINK=ocamlopt.opt
+CAMLMKTOP=ocamlmktop
+
+# Compilation debug flag
+CAMLDEBUG=
+
+# Compilation profile flag
+CAMLTIMEPROF=
+
+# The best compiler: native (=opt) or bytecode (=byte) if no native compiler
+BEST=opt
+
+# For Camlp4 use
+P4=$(COQTOP)/bin/$(ARCH)/call_camlp4 -I $(COQTOP)/src/parsing
+P4DEP=$(COQTOP)/bin/$(ARCH)/camlp4dep
+
+# Your architecture
+# Can be obtain by UNIX command arch
+ARCH=i686
+
+# Supplementary libs for some systems, currently:
+# . Sun Solaris: -cclib -lunix -cclib -lnsl -cclib -lsocket
+# . others : -cclib -lunix
+# . windows : -cclib -lunix
+
+OSDEPLIBS=-cclib -lunix
+
+# executable files extension, currently:
+# Unix systems:
+# Win32 systems : .exe
+EXE=
+
+# the command MKDIR (try to replace it with mkdirhier if you have problems)
+MKDIR=mkdir -p
+
+# where to put the coqdoc.sty style file
+COQDOCDIR=/usr/share/texmf/tex/latex/misc
+
+# command to update TeX' kpathsea database
+#MKTEXLSR=
+
+#the command STRIP
+# Unix systems and profiling: true
+# Unix systems and no profiling: strip
+# Win32 systems: true (actually strip is bogus)
+STRIP=strip
+
+# Options for reals (all/basic)
+REALS=all
+
+# CoqIde (no/byte/opt)
+HASCOQIDE=opt
+
+# make or sed are bogus and believe lines not terminating by a return
+# are inexistent
Modified: trunk/packages/coq-doc/branches/8.0pl3+8.1alpha/debian/changelog
URL: http://svn.debian.org/wsvn/pkg-ocaml-maint/trunk/packages/coq-doc/branches/8.0pl3%2B8.1alpha/debian/changelog?rev=2648&op=diff
==============================================================================
--- trunk/packages/coq-doc/branches/8.0pl3+8.1alpha/debian/changelog (original)
+++ trunk/packages/coq-doc/branches/8.0pl3+8.1alpha/debian/changelog Fri Apr 28 18:21:01 2006
@@ -1,9 +1,13 @@
-coq-doc (8.0pl1.0-2) unstable; urgency=low
+coq-doc (8.0pl3+8.1alpha-1) experimental; urgency=low
- * Split into -html and -ps, closes: #266019.
- * Moving to non-free since we don't have the sources for the documentation.
+ * The licensing issue is now solved. The new licence is OPL which is not
+ DFSG-compatible. We're moving to non-free, closes: #294865.
+ * Updated the copyright file.
+ * Split coq-doc into -html and -ps, closes: #266019.
+ * Using dpatch for handling patches.
+ * Updated standards version to 3.6.2, no changes needed.
- -- Samuel Mimram <smimram at debian.org> Wed, 5 Jan 2005 19:32:14 +0100
+ -- Samuel Mimram <smimram at debian.org> Fri, 28 Apr 2006 18:52:06 +0200
coq-doc (8.0pl1.0-1) unstable; urgency=low
Modified: trunk/packages/coq-doc/branches/8.0pl3+8.1alpha/debian/control
URL: http://svn.debian.org/wsvn/pkg-ocaml-maint/trunk/packages/coq-doc/branches/8.0pl3%2B8.1alpha/debian/control?rev=2648&op=diff
==============================================================================
--- trunk/packages/coq-doc/branches/8.0pl3+8.1alpha/debian/control (original)
+++ trunk/packages/coq-doc/branches/8.0pl3+8.1alpha/debian/control Fri Apr 28 18:21:01 2006
@@ -2,12 +2,12 @@
Section: non-free/doc
Priority: optional
Maintainer: Samuel Mimram <smimram at debian.org>
-Standards-Version: 3.6.1
-Build-Depends-Indep: debhelper (>= 4.0.0)
+Standards-Version: 3.6.2
+Build-Depends-Indep: debhelper (>= 4.0.0), dpatch, tetex-bin, hevea (>= 1.05), coq
Package: coq-doc
Architecture: all
-Depends: coq-doc-html coq-doc-ps
+Depends: coq-doc-html, coq-doc-ps
Description: documentation for Coq in html format
Coq is a proof assistant for higher-order logic, which allows the
development of computer programs consistent with their formal
Modified: trunk/packages/coq-doc/branches/8.0pl3+8.1alpha/debian/copyright
URL: http://svn.debian.org/wsvn/pkg-ocaml-maint/trunk/packages/coq-doc/branches/8.0pl3%2B8.1alpha/debian/copyright?rev=2648&op=diff
==============================================================================
--- trunk/packages/coq-doc/branches/8.0pl3+8.1alpha/debian/copyright (original)
+++ trunk/packages/coq-doc/branches/8.0pl3+8.1alpha/debian/copyright Fri Apr 28 18:21:01 2006
@@ -1,75 +1,174 @@
This package was debianized by Fernando Sanchez <fer at debian.org> on
Sun, 28 Nov 1999 19:42:06 +0100.
-The archive was created using files downloaded from
-http://coq.inria.fr/doc-eng.html
-The "Coq proof assistant" was developed conjointly by
- INRIA (since 1985),
- Laboratoire de l'Informatique du Parallelisme LIP
- associated to CNRS and ENS Lyon (sept.89-sept.97),
- Laboratoire de Recherche en Informatique
- associated to CNRS and Paris 11 (since sept. 97).
+The Coq Reference Manual is a collective work from the Coq Development
+Team whose members are listed in the file CREDITS of the Coq source
+package. All related documents (the LaTeX and BibTeX sources, the
+embedded png files, and the PostScript, PDF and html outputs) are
+copyright (c) INRIA 1999-2006. The material connected to the Reference
+Manual may be distributed only subject to the terms and conditions set
+forth in the Open Publication License, v1.0 or later (the latest
+version is presently available at http://www.opencontent.org/openpub/).
+Options A and B are *not* elected.
-The following people have contributed to the core of the system
-during the indicated time :
+The Coq Tutorial is a work by Gérard Huet, Gilles Kahn and Christine
+Paulin-Mohring. All documents (the LaTeX source and the PostScript,
+PDF and html outputs) are copyright (c) INRIA 1999-2006. The material
+connected to the Coq Tutorial may be distributed only subject to the
+terms and conditions set forth in the Open Publication License, v1.0
+or later (the latest version is presently available at
+http://www.opencontent.org/openpub/). Options A and B are *not*
+elected.
- Bruno Barras, (INRIA, 1995-1999)
- Cristina Cornes, (INRIA, 1993-1996)
- David Delahaye, (INRIA, 1997-1999)
- Daniel de Rauglaudre, (INRIA, 1996-1998)
- Jean-Christophe Filliâtre, (ENS Lyon, 1994-1997) (Paris 11,1997-1999)
- Eduardo Giménez, (ENS Lyon, 1993-1996, INRIA, 1997-1998)
- Hugo Herbelin, (INRIA, 1996-1999)
- Gérard Huet, (INRIA, 1985-1997)
- César Muñoz, (INRIA, 1994-1995)
- Chetan Murthy, (INRIA, 1992-1994)
- Catherine Parent-Vigouroux, (ENS Lyon 1992-1995)
- Patrick Loiseleur, (Paris 11, 1997-1999)
- Christine Paulin-Mohring, (INRIA, 1985-1989) (ENS Lyon, 1989-1997)
- (Paris 11, 1997-1999)
- Amokrane Saïbi, (INRIA, 1993-1998)
+The Coq Standard Library is a collective work from the Coq Development
+Team whose members are listed in the file CREDITS of the Coq source
+package. All related documents (the Coq vernacular source files and
+the PostScript, PDF and html outputs) are copyright (c) INRIA
+1999-2006. The material connected to the Standard Library is
+distributed under the terms of the Lesser General Public License
+version 2.1 or later.
+See /usr/share/common-licenses/LGPL.
-The following directories contain independent contributions:
-tactics/contrib/eqdecide
- developed by Eduardo Gimenez (INRIA, 1997-1998)
-tactics/contrib/extraction
- developed by Benjamin Werner (INRIA, 1989)
- and Jean-Christophe Filliatre (ENS Lyon, 1994-1997)
-tactics/contrib/linear
- developed by Jean-Christophe Filliatre (ENS Lyon, 1994-1997)
-tactics/contrib/natural
- developed by Yann Coscoy (INRIA, 1996)
-tactics/contrib/omega
- developed by Pierre Cregut (CNET-France Telecom, 1996)
-tactics/contrib/pcoq
- developed by Yves Bertot (INRIA, 1996-1999)
-tactics/contrib/polynom
- developed by Samuel Boutin (INRIA, 1996)
- and Patrick Loiseleur (LRI, 1997-1999)
-tactics/programs
- developed by Jean-Christophe Filliatre (LRI, 1997-1999)
-theories/REALS
- developed by Micaela Mayero (INRIA, 1997-1999)
-***************************************************************************
-INRIA refers to :
- Institute National de la Recherche en Informatique et Automatique
-CNRS refers to :
- Centre National de la Recherche Scientifique
-Paris 11 refers to :
- Universite Paris Sud
-ENS Lyon refers to :
- Ecole Normale Superieure de Lyon
-****************************************************************************
+The FAQ (Coq for the Clueless) is a work by Pierre Castéran, Hugo
+Herbelin, Florent Kirchner, Benjamin Monate, and Julien Narboux. All
+documents (the LaTeX source and the PostScript, PDF and html outputs)
+are copyright (c) INRIA 2004-2006. The material connected to the FAQ
+(Coq for the Clueless) may be distributed only subject to the terms
+and conditions set forth in the Open Publication License, v1.0 or
+later (the latest version is presently available at
+http://www.opencontent.org/openpub/). Options A and B are *not*
+elected.
+
+The Tutorial on [Co-]Inductive Types in Coq is a work by Pierre
+Castéran and Eduardo Gimenez. All related documents (the LaTeX and
+BibTeX sources and the PostScript, PDF and html outputs) are copyright
+(c) INRIA 1997-2006. The material connected to the Tutorial on
+[Co-]Inductive Types in Coq may be distributed only subject to the
+terms and conditions set forth in the Open Publication License, v1.0
+or later (the latest version is presently available at
+http://www.opencontent.org/openpub/). Options A and B are
+*not* elected.
+
+----------------------------------------------------------------------
+
+ *Open Publication License*
+ v1.0, 8 June 1999
-This documentation is freely available on the Coq web site: http://coq.inria.fr.
+*I. REQUIREMENTS ON BOTH UNMODIFIED AND MODIFIED VERSIONS*
-Copyright:
+The Open Publication works may be reproduced and distributed in whole or
+in part, in any medium physical or electronic, provided that the terms
+of this license are adhered to, and that this license or an
+incorporation of it by reference (with any options elected by the
+author(s) and/or publisher) is displayed in the reproduction.
-All files of the "Coq proof assistant" in directories or sub-directories of
- src, tactics, theories, tools
-are distributed under the terms of the GNU Lesser General Public License
-Version 2.1.
+Proper form for an incorporation by reference is as follows:
-See /usr/share/common-licenses/LGPL-2.1
+ Copyright (c) <year> by <author's name or designee>. This material
+ may be distributed only subject to the terms and conditions set
+ forth in the Open Publication License, vX.Y or later (the latest
+ version is presently available at http://www.opencontent.org/openpub/).
+
+The reference must be immediately followed with any options elected by
+the author(s) and/or publisher of the document (see section VI).
+
+Commercial redistribution of Open Publication-licensed material is
+permitted.
+
+Any publication in standard (paper) book form shall require the citation
+of the original publisher and author. The publisher and author's names
+shall appear on all outer surfaces of the book. On all outer surfaces of
+the book the original publisher's name shall be as large as the title of
+the work and cited as possessive with respect to the title.
+
+
+*II. COPYRIGHT*
+
+The copyright to each Open Publication is owned by its author(s) or
+designee.
+
+
+*III. SCOPE OF LICENSE*
+
+The following license terms apply to all Open Publication works, unless
+otherwise explicitly stated in the document.
+
+Mere aggregation of Open Publication works or a portion of an Open
+Publication work with other works or programs on the same media shall
+not cause this license to apply to those other works. The aggregate work
+shall contain a notice specifying the inclusion of the Open Publication
+material and appropriate copyright notice.
+
+SEVERABILITY. If any part of this license is found to be unenforceable
+in any jurisdiction, the remaining portions of the license remain in force.
+
+NO WARRANTY. Open Publication works are licensed and provided "as is"
+without warranty of any kind, express or implied, including, but not
+limited to, the implied warranties of merchantability and fitness for a
+particular purpose or a warranty of non-infringement.
+
+
+*IV. REQUIREMENTS ON MODIFIED WORKS*
+
+All modified versions of documents covered by this license, including
+translations, anthologies, compilations and partial documents, must meet
+the following requirements:
+
+ 1. The modified version must be labeled as such.
+ 2. The person making the modifications must be identified and the
+ modifications dated.
+ 3. Acknowledgement of the original author and publisher if applicable
+ must be retained according to normal academic citation practices.
+ 4. The location of the original unmodified document must be identified.
+ 5. The original author's (or authors') name(s) may not be used to
+ assert or imply endorsement of the resulting document without the
+ original author's (or authors') permission.
+
+
+*V. GOOD-PRACTICE RECOMMENDATIONS *
+
+In addition to the requirements of this license, it is requested from
+and strongly recommended of redistributors that:
+
+ 1. If you are distributing Open Publication works on hardcopy or
+ CD-ROM, you provide email notification to the authors of your
+ intent to redistribute at least thirty days before your manuscript
+ or media freeze, to give the authors time to provide updated
+ documents. This notification should describe modifications, if
+ any, made to the document.
+ 2. All substantive modifications (including deletions) be either
+ clearly marked up in the document or else described in an
+ attachment to the document.
+ 3. Finally, while it is not mandatory under this license, it is
+ considered good form to offer a free copy of any hardcopy and
+ CD-ROM expression of an Open Publication-licensed work to its
+ author(s).
+
+
+*VI. LICENSE OPTIONS*
+
+The author(s) and/or publisher of an Open Publication-licensed document
+may elect certain options by appending language to the reference to or
+copy of the license. These options are considered part of the license
+instance and must be included with the license (or its incorporation by
+reference) in derived works.
+
+A. To prohibit distribution of substantively modified versions without
+the explicit permission of the author(s). "Substantive modification" is
+defined as a change to the semantic content of the document, and
+excludes mere changes in format or typographical corrections.
+
+To accomplish this, add the phrase `Distribution of substantively
+modified versions of this document is prohibited without the explicit
+permission of the copyright holder.' to the license reference or copy.
+
+B. To prohibit any publication of this work or derivative works in whole
+or in part in standard (paper) book form for commercial purposes is
+prohibited unless prior permission is obtained from the copyright holder.
+
+To accomplish this, add the phrase 'Distribution of the work or
+derivative of the work in any standard (paper) book form is prohibited
+unless prior permission is obtained from the copyright holder.' to the
+license reference or copy.
Added: trunk/packages/coq-doc/branches/8.0pl3+8.1alpha/debian/patches/00list
URL: http://svn.debian.org/wsvn/pkg-ocaml-maint/trunk/packages/coq-doc/branches/8.0pl3%2B8.1alpha/debian/patches/00list?rev=2648&op=file
==============================================================================
--- trunk/packages/coq-doc/branches/8.0pl3+8.1alpha/debian/patches/00list (added)
+++ trunk/packages/coq-doc/branches/8.0pl3+8.1alpha/debian/patches/00list Fri Apr 28 18:21:01 2006
@@ -1,0 +1,1 @@
+config_makefile
Added: trunk/packages/coq-doc/branches/8.0pl3+8.1alpha/debian/patches/config_makefile.dpatch
URL: http://svn.debian.org/wsvn/pkg-ocaml-maint/trunk/packages/coq-doc/branches/8.0pl3%2B8.1alpha/debian/patches/config_makefile.dpatch?rev=2648&op=file
==============================================================================
--- trunk/packages/coq-doc/branches/8.0pl3+8.1alpha/debian/patches/config_makefile.dpatch (added)
+++ trunk/packages/coq-doc/branches/8.0pl3+8.1alpha/debian/patches/config_makefile.dpatch Fri Apr 28 18:21:01 2006
@@ -1,0 +1,19 @@
+#! /bin/sh /usr/share/dpatch/dpatch-run
+## config_makefile.dpatch by Samuel Mimram <smimram at debian.org>
+##
+## All lines beginning with `## DP:' are a description of the patch.
+## DP: Use a custom configuration for the Makefile.
+
+ at DPATCH@
+diff -urNad coq-doc-8.0pl3+8.1alpha~/Makefile coq-doc-8.0pl3+8.1alpha/Makefile
+--- coq-doc-8.0pl3+8.1alpha~/Makefile 2006-04-28 18:50:58.000000000 +0200
++++ coq-doc-8.0pl3+8.1alpha/Makefile 2006-04-28 19:10:54.000000000 +0200
+@@ -7,7 +7,7 @@
+ # Pdf: pdflatex
+ # Html: hevea (http://hevea.inria.fr) >= 1.05
+
+-include ../config/Makefile
++include debian/Makefile.config
+
+
+ LATEX=latex
Propchange: trunk/packages/coq-doc/branches/8.0pl3+8.1alpha/debian/patches/config_makefile.dpatch
------------------------------------------------------------------------------
svn:executable = *
Modified: trunk/packages/coq-doc/branches/8.0pl3+8.1alpha/debian/rules
URL: http://svn.debian.org/wsvn/pkg-ocaml-maint/trunk/packages/coq-doc/branches/8.0pl3%2B8.1alpha/debian/rules?rev=2648&op=diff
==============================================================================
--- trunk/packages/coq-doc/branches/8.0pl3+8.1alpha/debian/rules (original)
+++ trunk/packages/coq-doc/branches/8.0pl3+8.1alpha/debian/rules Fri Apr 28 18:21:01 2006
@@ -4,9 +4,14 @@
# Uncomment this to turn on verbose mode.
#export DH_VERBOSE=1
-build:
+# We want to use dpatch
+include /usr/share/dpatch/dpatch.make
-clean:
+build: patch-stamp
+ $(MAKE) tutorial/Tutorial.v.html refman/html/index.html faq/html/index.html RecTutorial/RecTutorial.v.html
+ $(MAKE) tutorial/Tutorial.v.pdf refman/Reference-Manual.pdf faq/FAQ.v.pdf RecTutorial/RecTutorial.v.pdf
+
+clean: unpatch
dh_testdir
dh_testroot
dh_clean
Added: trunk/packages/coq-doc/branches/upstream/coq-doc_8.0pl3+8.1alpha.orig.tar.gz
URL: http://svn.debian.org/wsvn/pkg-ocaml-maint/trunk/packages/coq-doc/branches/upstream/coq-doc_8.0pl3%2B8.1alpha.orig.tar.gz?rev=2648&op=file
==============================================================================
Binary file - no diff available.
Propchange: trunk/packages/coq-doc/branches/upstream/coq-doc_8.0pl3+8.1alpha.orig.tar.gz
------------------------------------------------------------------------------
svn:mime-type = application/octet-stream
Modified: trunk/packages/coq-doc/trunk/debian/changelog
URL: http://svn.debian.org/wsvn/pkg-ocaml-maint/trunk/packages/coq-doc/trunk/debian/changelog?rev=2648&op=diff
==============================================================================
--- trunk/packages/coq-doc/trunk/debian/changelog (original)
+++ trunk/packages/coq-doc/trunk/debian/changelog Fri Apr 28 18:21:01 2006
@@ -1,9 +1,13 @@
-coq-doc (8.0pl1.0-2) unstable; urgency=low
+coq-doc (8.0pl1.0-2) UNRELEASED; urgency=low
- * Split into -html and -ps, closes: #266019.
+ * NOT RELEASED YET
+ * The licensing issue is now solved. Updated the copyright file,
+ closes: #294865.
* Moving to non-free since we don't have the sources for the documentation.
+ * Split coq-doc into -html and -ps, closes: #266019.
+ * Updated standards version to 3.6.2, no changes needed.
- -- Samuel Mimram <smimram at debian.org> Wed, 5 Jan 2005 19:32:14 +0100
+ -- Samuel Mimram <smimram at debian.org> Tue, 27 Dec 2005 17:27:54 +0100
coq-doc (8.0pl1.0-1) unstable; urgency=low
Modified: trunk/packages/coq-doc/trunk/debian/control
URL: http://svn.debian.org/wsvn/pkg-ocaml-maint/trunk/packages/coq-doc/trunk/debian/control?rev=2648&op=diff
==============================================================================
--- trunk/packages/coq-doc/trunk/debian/control (original)
+++ trunk/packages/coq-doc/trunk/debian/control Fri Apr 28 18:21:01 2006
@@ -2,12 +2,12 @@
Section: non-free/doc
Priority: optional
Maintainer: Samuel Mimram <smimram at debian.org>
-Standards-Version: 3.6.1
+Standards-Version: 3.6.2
Build-Depends-Indep: debhelper (>= 4.0.0)
Package: coq-doc
Architecture: all
-Depends: coq-doc-html coq-doc-ps
+Depends: coq-doc-html, coq-doc-ps
Description: documentation for Coq in html format
Coq is a proof assistant for higher-order logic, which allows the
development of computer programs consistent with their formal
More information about the Pkg-ocaml-maint-commits
mailing list