diff options
| -rw-r--r-- | contrib/xml/xmlcommand.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml index cbb25bed67..4aa22a71b3 100644 --- a/contrib/xml/xmlcommand.ml +++ b/contrib/xml/xmlcommand.ml @@ -14,7 +14,7 @@ let dtdname = "http://localhost:8081/getdtd?uri=cic.dtd";; let typesdtdname = "http://localhost:8081/getdtd?uri=cictypes.dtd";; -let verbose = ref true;; (* always set to true during a "Print XML All" *) +let verbose = ref false;; (* always set to true during a "Print XML All" *) (* UTILITY FUNCTIONS *) |