From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 27 Nov 2001 17:05:01 +0000 (+0000)
Subject: annotations: was yes or NO. It is now yes or no.
X-Git-Tag: mlminidom_0_2_2~53
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=8efd7ae18e1a9555e66254a39afadce56b74c42d;p=helm.git

annotations: was yes or NO. It is now yes or no.
---

diff --git a/helm/annotationHelper/cicAnnotationHelper.ml b/helm/annotationHelper/cicAnnotationHelper.ml
index 3104f6e66..0b858b268 100644
--- a/helm/annotationHelper/cicAnnotationHelper.ml
+++ b/helm/annotationHelper/cicAnnotationHelper.ml
@@ -101,7 +101,7 @@ module UrlManipulator =
                  Some
                   (match ann with
                       "yes" -> ".ann"
-                    | "NO"  -> ""
+                    | "no"  -> ""
                     | _     -> raise (Bad_formed_url url)
                   ) ;
                 if !founduri = None then