diff options
| author | ppedrot | 2012-11-13 22:38:16 +0000 |
|---|---|---|
| committer | ppedrot | 2012-11-13 22:38:16 +0000 |
| commit | 98f3621b5b0c50aaa48c86e1d6a4269d94388bd3 (patch) | |
| tree | e7ecad4d80598956e9aeda2f5c82302ab7e0bde8 /lib/system.ml | |
| parent | 1d436a18f2f72b57ea09a6d27709a36b63be863a (diff) | |
More monomorphizations
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15969 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'lib/system.ml')
| -rw-r--r-- | lib/system.ml | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/lib/system.ml b/lib/system.ml index 84706d0313..a2b371b1fc 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -24,7 +24,7 @@ let exclude_search_in_dirname f = skipped_dirnames := f :: !skipped_dirnames let ok_dirname f = f <> "" && f.[0] <> '.' && not (List.mem f !skipped_dirnames) && - (Unicode.ident_refutation f = None) + (match Unicode.ident_refutation f with None -> true | _ -> false) let all_subdirs ~unix_path:root = let l = ref [] in @@ -37,11 +37,13 @@ let all_subdirs ~unix_path:root = if ok_dirname f then let file = Filename.concat dir f in try - if (stat file).st_kind = S_DIR then begin - let newrel = rel@[f] in + begin match (stat file).st_kind with + | S_DIR -> + let newrel = rel @ [f] in add file newrel; traverse file newrel - end + | _ -> () + end with Unix_error (e,s1,s2) -> () done with End_of_file -> |