From 69395e449f16e78e00be27b56ef55a3b19464ba2 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 26 Mar 2004 16:43:34 +0000
Subject: Ajout option raw-comments pour supprimer affichage de <table>

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5580 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tools/coqdoc/output.mli | 1 +
 1 file changed, 1 insertion(+)

(limited to 'tools')

diff --git a/tools/coqdoc/output.mli b/tools/coqdoc/output.mli
index 5b1136e5c5..0da9669420 100644
--- a/tools/coqdoc/output.mli
+++ b/tools/coqdoc/output.mli
@@ -28,6 +28,7 @@ val toc : bool ref
 val title : string ref
 val externals : bool ref
 val coqlib : string ref
+val raw_comments : bool ref
 
 val charset : string ref
 val inputenc : string ref
-- 
cgit v1.2.3