aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/xml
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2000-11-28 16:32:08 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2000-11-28 16:32:08 +0000
commit7da58295173715d6de518516e2653dac90dd2d5c (patch)
tree2cba748ef7c3c437fb527fe15214d02b2f546e14 /contrib/xml
parent14b236a0bcc5071c5048d87768437df0b30e387a (diff)
Prise en compte du repertoire dans le section path; utilisation de dirpath pour les noms de modules
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1005 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/xml')
-rw-r--r--contrib/xml/xmlcommand.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml
index df79fe3f7..62f7020a1 100644
--- a/contrib/xml/xmlcommand.ml
+++ b/contrib/xml/xmlcommand.ml
@@ -847,7 +847,7 @@ and print_node n id sp bprintleaf dn =
end ;
print_if_verbose "/ClosedDir\n"
| L.Module s ->
- print_if_verbose ("Module " ^ s ^ "\n")
+ print_if_verbose ("Module " ^ (Names.string_of_dirpath s) ^ "\n")
| L.FrozenState _ ->
print_if_verbose ("FrozenState\n")
;;