diff options
| author |  Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2013-12-03 09:55:04 +0100 |
|---|---|---|
| committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2013-12-03 09:55:04 +0100 |
| commit | 1e5e934a8ce31c129368e57b61e485e6b989c3f4 (patch) | |
| tree | 5ea4ce12c4faf03b631f452e4a362eb40bc422b5 /ide/wg_Completion.ml | |
| parent | 24d17c1084d0926047b7ce5c7e3adac43f62378a (diff) | |
Silence compilation warning by avoiding some deprecated constructs.
Diffstat (limited to 'ide/wg_Completion.ml')
| -rw-r--r-- | ide/wg_Completion.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/ide/wg_Completion.ml b/ide/wg_Completion.ml index 7317f1abc..43564ba57 100644 --- a/ide/wg_Completion.ml +++ b/ide/wg_Completion.ml @@ -60,7 +60,7 @@ let is_substring s1 s2 = let i = ref 0 in let len1 = Array.length s1 in let len2 = Array.length s2 in - while !break && !i < len1 & !i < len2 do + while !break && !i < len1 && !i < len2 do break := s1.(!i) = s2.(!i); incr i; done; |