summaryrefslogtreecommitdiff
path: root/contrib/interface/paths.ml
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/interface/paths.ml')
-rw-r--r--contrib/interface/paths.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/interface/paths.ml b/contrib/interface/paths.ml
index b1244d15..a157ca92 100644
--- a/contrib/interface/paths.ml
+++ b/contrib/interface/paths.ml
@@ -23,4 +23,4 @@ let rec lex_smaller p1 p2 = match p1,p2 with
[], _ -> true
| a::tl1, b::tl2 when a < b -> true
| a::tl1, b::tl2 when a = b -> lex_smaller tl1 tl2
-| _ -> false;; \ No newline at end of file
+| _ -> false;;