From de8e041c0c9ced8f91e934255de6a925bdcd9d0a Mon Sep 17 00:00:00 2001 From: notin Date: Thu, 23 Mar 2006 10:08:22 +0000 Subject: Correction d'un bug sur 'make doc' et modification des propriétés dans doc/ git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8656 85f007b7-540e-0410-9357-904b9bb8a0f7 --- Makefile | 2 +- configure | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/Makefile b/Makefile index ebafe9f33a..e6b5be6c1a 100644 --- a/Makefile +++ b/Makefile @@ -1258,7 +1258,7 @@ install-latex: .PHONY: doc devdoc -doc: coq +doc: glob.dump (cd doc; make all) clean:: diff --git a/configure b/configure index db73e56c0c..0879de1ab6 100755 --- a/configure +++ b/configure @@ -6,8 +6,8 @@ # ################################## -VERSION=8.0cvs -DATE="Apr 2004" +VERSION=trunk +DATE="Mar 2006" # a local which command for sh which () { -- cgit v1.2.3