diff options
| -rw-r--r-- | Makefile | 2 | ||||
| -rwxr-xr-x | configure | 4 |
2 files changed, 3 insertions, 3 deletions
@@ -1258,7 +1258,7 @@ install-latex: .PHONY: doc devdoc -doc: coq +doc: glob.dump (cd doc; make all) clean:: @@ -6,8 +6,8 @@ # ################################## -VERSION=8.0cvs -DATE="Apr 2004" +VERSION=trunk +DATE="Mar 2006" # a local which command for sh which () { |
