diff options
Diffstat (limited to 'parsing/g_ascii_syntax.ml')
| -rw-r--r-- | parsing/g_ascii_syntax.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/parsing/g_ascii_syntax.ml b/parsing/g_ascii_syntax.ml index 8c570b0fd..f9ca94ff6 100644 --- a/parsing/g_ascii_syntax.ml +++ b/parsing/g_ascii_syntax.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(*i $Id:$ i*) +(*i $Id$ i*) open Pp open Util @@ -53,7 +53,7 @@ let interp_ascii_string dloc s = then int_of_string s else user_err_loc (dloc,"interp_ascii_string", - str "Expects a single character or a three-digits ascii code") in + str "Expects a single character or a three-digits ascii code.") in interp_ascii dloc p let uninterp_ascii r = |