aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib
diff options
context:
space:
mode:
authorGravatar Pierre Letouzey <pierre.letouzey@inria.fr>2014-12-09 12:48:32 +0100
committerGravatar Pierre Letouzey <pierre.letouzey@inria.fr>2014-12-09 14:27:21 +0100
commitaf84e080ff674a3d5cf2cf88874ddb6ebaf38ecf (patch)
treeb8325cd8ce34dd2dcfba2792a0123cf8c46ab703 /lib
parent9c24cecec3a7381cd924c56ca50c77a49750e2e5 (diff)
Switch the few remaining iso-latin-1 files to utf8
Diffstat (limited to 'lib')
-rw-r--r--lib/explore.ml2
-rw-r--r--lib/pp.ml2
2 files changed, 2 insertions, 2 deletions
diff --git a/lib/explore.ml b/lib/explore.ml
index 90258b0e5..984114bf1 100644
--- a/lib/explore.ml
+++ b/lib/explore.ml
@@ -50,7 +50,7 @@ module Make = functor(S : SearchProblem) -> struct
in
explore [1] s
- (*s Breadth first search. We use functional FIFOS à la Okasaki. *)
+ (*s Breadth first search. We use functional FIFOS à la Okasaki. *)
type 'a queue = 'a list * 'a list
diff --git a/lib/pp.ml b/lib/pp.ml
index 405eacffe..d7ae31dd3 100644
--- a/lib/pp.ml
+++ b/lib/pp.ml
@@ -167,7 +167,7 @@ let rewrite f p =
Rem 2 : if used for an iso8859_1 encoded string, the result is
wrong in very rare cases. Such a wrong case corresponds to any
sequence of a character in range 192..253 immediately followed by a
- character in range 128..191 (typical case in french is "déçu" which
+ character in range 128..191 (typical case in french is "déçu" which
is counted 3 instead of 4); then no real harm to use always
utf8_length even if using an iso8859_1 encoding *)