[Pkg-ocaml-maint-commits] r2941 - in /trunk/packages/coq-doc:
branches/ trunk/debian/ trunk/debian/patches/ upstream/
smimram at users.alioth.debian.org
smimram at users.alioth.debian.org
Thu Jul 13 16:51:21 UTC 2006
Author: smimram
Date: Thu Jul 13 16:51:19 2006
New Revision: 2941
URL: http://svn.debian.org/wsvn/pkg-ocaml-maint/?sc=1&rev=2941
Log:
New beta upstream release.
Added:
trunk/packages/coq-doc/trunk/debian/Makefile.config
trunk/packages/coq-doc/trunk/debian/coq-doc-html.doc-base.rectutorial
trunk/packages/coq-doc/trunk/debian/coq-doc-pdf.dirs
trunk/packages/coq-doc/trunk/debian/coq-doc-pdf.docs
trunk/packages/coq-doc/trunk/debian/patches/
trunk/packages/coq-doc/trunk/debian/patches/00list
trunk/packages/coq-doc/trunk/debian/patches/config_makefile.dpatch (with props)
trunk/packages/coq-doc/upstream/coq-doc_8.0pl3+8.1beta.2.orig.tar.gz (with props)
Removed:
trunk/packages/coq-doc/branches/
trunk/packages/coq-doc/upstream/coq-doc_8.0pl1.0.orig.tar.gz
Modified:
trunk/packages/coq-doc/trunk/debian/changelog
trunk/packages/coq-doc/trunk/debian/control
trunk/packages/coq-doc/trunk/debian/copyright
trunk/packages/coq-doc/trunk/debian/coq-doc-html.dirs
trunk/packages/coq-doc/trunk/debian/coq-doc-html.doc-base.faq
trunk/packages/coq-doc/trunk/debian/coq-doc-html.doc-base.manual
trunk/packages/coq-doc/trunk/debian/coq-doc-html.doc-base.tutorial
trunk/packages/coq-doc/trunk/debian/coq-doc-html.docs
trunk/packages/coq-doc/trunk/debian/rules
Added: trunk/packages/coq-doc/trunk/debian/Makefile.config
URL: http://svn.debian.org/wsvn/pkg-ocaml-maint/trunk/packages/coq-doc/trunk/debian/Makefile.config?rev=2941&op=file
==============================================================================
--- trunk/packages/coq-doc/trunk/debian/Makefile.config (added)
+++ trunk/packages/coq-doc/trunk/debian/Makefile.config Thu Jul 13 16:51:19 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/trunk/debian/changelog
URL: http://svn.debian.org/wsvn/pkg-ocaml-maint/trunk/packages/coq-doc/trunk/debian/changelog?rev=2941&op=diff
==============================================================================
--- trunk/packages/coq-doc/trunk/debian/changelog (original)
+++ trunk/packages/coq-doc/trunk/debian/changelog Thu Jul 13 16:51:19 2006
@@ -1,13 +1,27 @@
-coq-doc (8.0pl1.0-2) UNRELEASED; urgency=low
+coq-doc (8.0pl3+8.1beta.2-1) experimental; urgency=low
- * 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.
+ * New beta upstream release.
+
+ -- Samuel Mimram <smimram at debian.org> Thu, 13 Jul 2006 14:40:04 +0000
+
+coq-doc (8.0pl3+8.1alpha-2) experimental; urgency=low
+
+ * Correct a typo in coq-rectutorial's doc-base (thanks Remi Vanicat),
+ closes: #366611.
+ * Updated standards version to 3.7.2, no changes needed.
+
+ -- Samuel Mimram <smimram at debian.org> Wed, 10 May 2006 16:39:24 +0000
+
+coq-doc (8.0pl3+8.1alpha-1) experimental; urgency=low
+
+ * 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 -pdf, closes: #266019.
+ * Using dpatch for handling patches.
* Updated standards version to 3.6.2, no changes needed.
- -- Samuel Mimram <smimram at debian.org> Tue, 27 Dec 2005 17:27:54 +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/trunk/debian/control
URL: http://svn.debian.org/wsvn/pkg-ocaml-maint/trunk/packages/coq-doc/trunk/debian/control?rev=2941&op=diff
==============================================================================
--- trunk/packages/coq-doc/trunk/debian/control (original)
+++ trunk/packages/coq-doc/trunk/debian/control Thu Jul 13 16:51:19 2006
@@ -2,12 +2,13 @@
Section: non-free/doc
Priority: optional
Maintainer: Samuel Mimram <smimram at debian.org>
-Standards-Version: 3.6.2
-Build-Depends-Indep: debhelper (>= 4.0.0)
+Standards-Version: 3.7.2
+Build-Depends: debhelper (>= 4.0.0), dpatch
+Build-Depends-Indep: tetex-bin, hevea (>= 1.05), coq (>= 8.0)
Package: coq-doc
Architecture: all
-Depends: coq-doc-html, coq-doc-ps
+Depends: coq-doc-html, coq-doc-pdf
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
@@ -28,13 +29,13 @@
.
This package contains its documentation and tutorials in html format.
-Package: coq-doc-ps
+Package: coq-doc-pdf
Architecture: all
Replaces: coq-doc (<= 8.0pl1.0-1)
-Description: documentation for Coq in postscript format
+Description: documentation for Coq in pdf format
Coq is a proof assistant for higher-order logic, which allows the
development of computer programs consistent with their formal
specification. It is developed using Objective Caml and Camlp4.
For more information, see <http://coq.inria.fr/>.
.
- This package contains its documentation and tutorials in postscript format.
+ This package contains its documentation and tutorials in pdf format.
Modified: trunk/packages/coq-doc/trunk/debian/copyright
URL: http://svn.debian.org/wsvn/pkg-ocaml-maint/trunk/packages/coq-doc/trunk/debian/copyright?rev=2941&op=diff
==============================================================================
--- trunk/packages/coq-doc/trunk/debian/copyright (original)
+++ trunk/packages/coq-doc/trunk/debian/copyright Thu Jul 13 16:51:19 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.
Modified: trunk/packages/coq-doc/trunk/debian/coq-doc-html.dirs
URL: http://svn.debian.org/wsvn/pkg-ocaml-maint/trunk/packages/coq-doc/trunk/debian/coq-doc-html.dirs?rev=2941&op=diff
==============================================================================
--- trunk/packages/coq-doc/trunk/debian/coq-doc-html.dirs (original)
+++ trunk/packages/coq-doc/trunk/debian/coq-doc-html.dirs Thu Jul 13 16:51:19 2006
@@ -1,2 +1,2 @@
usr/share/doc/coq
-usr/share/doc/coq-doc-html
+usr/share/doc/coq-doc-html/refman
Modified: trunk/packages/coq-doc/trunk/debian/coq-doc-html.doc-base.faq
URL: http://svn.debian.org/wsvn/pkg-ocaml-maint/trunk/packages/coq-doc/trunk/debian/coq-doc-html.doc-base.faq?rev=2941&op=diff
==============================================================================
--- trunk/packages/coq-doc/trunk/debian/coq-doc-html.doc-base.faq (original)
+++ trunk/packages/coq-doc/trunk/debian/coq-doc-html.doc-base.faq Thu Jul 13 16:51:19 2006
@@ -5,5 +5,5 @@
Section: Apps/Math
Format: HTML
-Index: /usr/share/doc/coq-doc-html/faq.html
-Files: /usr/share/doc/coq-doc-html/faq.html
+Index: /usr/share/doc/coq-doc-html/FAQ.v.html
+Files: /usr/share/doc/coq-doc-html/FAQ.v.html
Modified: trunk/packages/coq-doc/trunk/debian/coq-doc-html.doc-base.manual
URL: http://svn.debian.org/wsvn/pkg-ocaml-maint/trunk/packages/coq-doc/trunk/debian/coq-doc-html.doc-base.manual?rev=2941&op=diff
==============================================================================
--- trunk/packages/coq-doc/trunk/debian/coq-doc-html.doc-base.manual (original)
+++ trunk/packages/coq-doc/trunk/debian/coq-doc-html.doc-base.manual Thu Jul 13 16:51:19 2006
@@ -5,5 +5,5 @@
Section: Apps/Math
Format: HTML
-Index: /usr/share/doc/coq-doc-html/manual/index.html
-Files: /usr/share/doc/coq-doc-html/manual/*.html
+Index: /usr/share/doc/coq-doc-html/refman/index.html
+Files: /usr/share/doc/coq-doc-html/refman/*.html
Added: trunk/packages/coq-doc/trunk/debian/coq-doc-html.doc-base.rectutorial
URL: http://svn.debian.org/wsvn/pkg-ocaml-maint/trunk/packages/coq-doc/trunk/debian/coq-doc-html.doc-base.rectutorial?rev=2941&op=file
==============================================================================
--- trunk/packages/coq-doc/trunk/debian/coq-doc-html.doc-base.rectutorial (added)
+++ trunk/packages/coq-doc/trunk/debian/coq-doc-html.doc-base.rectutorial Thu Jul 13 16:51:19 2006
@@ -1,0 +1,9 @@
+Document: coq-rectutorial
+Title: The Coq Proof Assistant -- A Tutorial on [Co-]Inductive types in Coq
+Author: Eduardo Giménez and Pierre Castéran
+Abstract: This document is an introduction to the definition and use of inductive and co-inductive types in the Coq proof environment. It explains how types like natural numbers and infinite streams are defined in Coq, and the kind of proof techniques that can be used to reason about them (case analysis, induction, inversion of predicates, co-induction, etc). Each technique is illustrated through an executable and self-contained Coq script.
+Section: Apps/Math
+
+Format: HTML
+Index: /usr/share/doc/coq-doc-html/RecTutorial.v.html
+Files: /usr/share/doc/coq-doc-html/RecTutorial.v.html
Modified: trunk/packages/coq-doc/trunk/debian/coq-doc-html.doc-base.tutorial
URL: http://svn.debian.org/wsvn/pkg-ocaml-maint/trunk/packages/coq-doc/trunk/debian/coq-doc-html.doc-base.tutorial?rev=2941&op=diff
==============================================================================
--- trunk/packages/coq-doc/trunk/debian/coq-doc-html.doc-base.tutorial (original)
+++ trunk/packages/coq-doc/trunk/debian/coq-doc-html.doc-base.tutorial Thu Jul 13 16:51:19 2006
@@ -5,5 +5,5 @@
Section: Apps/Math
Format: HTML
-Index: /usr/share/doc/coq-doc-html/tutorial.html
-Files: /usr/share/doc/coq-doc-html/tutorial.html
+Index: /usr/share/doc/coq-doc-html/Tutorial.v.html
+Files: /usr/share/doc/coq-doc-html/Tutorial.v.html
Modified: trunk/packages/coq-doc/trunk/debian/coq-doc-html.docs
URL: http://svn.debian.org/wsvn/pkg-ocaml-maint/trunk/packages/coq-doc/trunk/debian/coq-doc-html.docs?rev=2941&op=diff
==============================================================================
--- trunk/packages/coq-doc/trunk/debian/coq-doc-html.docs (original)
+++ trunk/packages/coq-doc/trunk/debian/coq-doc-html.docs Thu Jul 13 16:51:19 2006
@@ -1,4 +1,0 @@
-library
-manual
-tutorial.html
-faq.html
Added: trunk/packages/coq-doc/trunk/debian/coq-doc-pdf.dirs
URL: http://svn.debian.org/wsvn/pkg-ocaml-maint/trunk/packages/coq-doc/trunk/debian/coq-doc-pdf.dirs?rev=2941&op=file
==============================================================================
--- trunk/packages/coq-doc/trunk/debian/coq-doc-pdf.dirs (added)
+++ trunk/packages/coq-doc/trunk/debian/coq-doc-pdf.dirs Thu Jul 13 16:51:19 2006
@@ -1,0 +1,2 @@
+usr/share/doc/coq
+usr/share/doc/coq-doc-pdf
Added: trunk/packages/coq-doc/trunk/debian/coq-doc-pdf.docs
URL: http://svn.debian.org/wsvn/pkg-ocaml-maint/trunk/packages/coq-doc/trunk/debian/coq-doc-pdf.docs?rev=2941&op=file
==============================================================================
--- trunk/packages/coq-doc/trunk/debian/coq-doc-pdf.docs (added)
+++ trunk/packages/coq-doc/trunk/debian/coq-doc-pdf.docs Thu Jul 13 16:51:19 2006
@@ -1,0 +1,4 @@
+tutorial/Tutorial.v.pdf
+refman/Reference-Manual.pdf
+faq/FAQ.v.pdf
+RecTutorial/RecTutorial.v.pdf
Added: trunk/packages/coq-doc/trunk/debian/patches/00list
URL: http://svn.debian.org/wsvn/pkg-ocaml-maint/trunk/packages/coq-doc/trunk/debian/patches/00list?rev=2941&op=file
==============================================================================
--- trunk/packages/coq-doc/trunk/debian/patches/00list (added)
+++ trunk/packages/coq-doc/trunk/debian/patches/00list Thu Jul 13 16:51:19 2006
@@ -1,0 +1,1 @@
+config_makefile
Added: trunk/packages/coq-doc/trunk/debian/patches/config_makefile.dpatch
URL: http://svn.debian.org/wsvn/pkg-ocaml-maint/trunk/packages/coq-doc/trunk/debian/patches/config_makefile.dpatch?rev=2941&op=file
==============================================================================
--- trunk/packages/coq-doc/trunk/debian/patches/config_makefile.dpatch (added)
+++ trunk/packages/coq-doc/trunk/debian/patches/config_makefile.dpatch Thu Jul 13 16:51:19 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/trunk/debian/patches/config_makefile.dpatch
------------------------------------------------------------------------------
svn:executable = *
Modified: trunk/packages/coq-doc/trunk/debian/rules
URL: http://svn.debian.org/wsvn/pkg-ocaml-maint/trunk/packages/coq-doc/trunk/debian/rules?rev=2941&op=diff
==============================================================================
--- trunk/packages/coq-doc/trunk/debian/rules (original)
+++ trunk/packages/coq-doc/trunk/debian/rules Thu Jul 13 16:51:19 2006
@@ -4,9 +4,16 @@
# Uncomment this to turn on verbose mode.
#export DH_VERBOSE=1
-build:
+# We want to use dpatch
+include /usr/share/dpatch/dpatch.make
-clean:
+HTMLDEST := $(CURDIR)/debian/coq-doc-html/usr/share/doc/coq-doc-html/
+
+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
@@ -18,10 +25,13 @@
dh_installdirs
dh_installdocs
- cd debian/coq-doc-html/usr/share/doc/coq-doc-html/manual; ln -s main.html index.html
- cd debian/coq-doc-html/usr/share/doc/coq; ln -s ../coq-doc-html html;
- cd debian/coq-doc-ps/usr/share/doc/coq; ln -s ../coq-doc-ps ps
- cd debian/coq-doc/usr/share/doc/coq-doc; ln -s ../coq-doc-html html; ln -s ../coq-doc-ps ps
+ cp tutorial/Tutorial.v.html $(HTMLDEST)
+ cp refman/*.html $(HTMLDEST)/refman
+ cp faq/FAQ.v.html $(HTMLDEST)
+ cp RecTutorial/RecTutorial.v.html $(HTMLDEST)
+ cd debian/coq-doc-html/usr/share/doc/coq; ln -s ../coq-doc-html html
+ cd debian/coq-doc-pdf/usr/share/doc/coq; ln -s ../coq-doc-pdf pdf
+ cd debian/coq-doc/usr/share/doc/coq-doc; ln -s ../coq-doc-html html; ln -s ../coq-doc-pdf pdf
touch install-stamp
@@ -36,7 +46,7 @@
dh_installchangelogs
dh_link
dh_strip
- dh_compress
+ dh_compress -X.pdf
dh_fixperms
dh_installdeb
dh_gencontrol
Added: trunk/packages/coq-doc/upstream/coq-doc_8.0pl3+8.1beta.2.orig.tar.gz
URL: http://svn.debian.org/wsvn/pkg-ocaml-maint/trunk/packages/coq-doc/upstream/coq-doc_8.0pl3%2B8.1beta.2.orig.tar.gz?rev=2941&op=file
==============================================================================
Binary file - no diff available.
Propchange: trunk/packages/coq-doc/upstream/coq-doc_8.0pl3+8.1beta.2.orig.tar.gz
------------------------------------------------------------------------------
svn:mime-type = application/octet-stream
More information about the Pkg-ocaml-maint-commits
mailing list