aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/heads.ml
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2008-04-24 07:19:57 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2008-04-24 07:19:57 +0000
commit960efee9230e8aff4817668f918039f768018f09 (patch)
tree137658ff6942cf82e6e8fdb31cf1c147d7823139 /library/heads.ml
parent37c82d53d56816c1f01062abd20c93e6a22ee924 (diff)
Ajout propriété svn:keywords aux nouveaux fichiers du commit 10840
(~/.subversion/config n'avait pas la ligne magique "* = svn:keywords=Author Date Id Revision" dans la section [auto-props]). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10841 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library/heads.ml')
-rw-r--r--library/heads.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/library/heads.ml b/library/heads.ml
index c341c835e..ca1f1014f 100644
--- a/library/heads.ml
+++ b/library/heads.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id:$ *)
+(* $Id$ *)
open Pp
open Util