From 7e79f902b0fea9afb02576b653b384bc512b2264 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 2 Sep 2008 13:59:47 +0000 Subject: [PATCH] Uri ending in '' were not accepted. Fixed. --- helm/software/components/grafite_parser/grafiteParser.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml index b9f6d388f..0dd5c0885 100644 --- a/helm/software/components/grafite_parser/grafiteParser.ml +++ b/helm/software/components/grafite_parser/grafiteParser.ml @@ -537,7 +537,8 @@ EXTEND let alpha = "[a-zA-Z]" in let num = "[0-9]+" in let ident_cont = "\\("^alpha^"\\|"^num^"\\|_\\|\\\\\\)" in - let ident = "\\("^alpha^ident_cont^"*\\|_"^ident_cont^"+\\)" in + let decoration = "\\'" in + let ident = "\\("^alpha^ident_cont^"*"^decoration^"*\\|_"^ident_cont^"+"^decoration^"*\\)" in let rex = Str.regexp ("^"^ident^"$") in if Str.string_match rex id 0 then if (try ignore (UriManager.uri_of_string uri); true -- 2.39.2