diff options
| -rw-r--r-- | lib/util.ml | 7 |
1 files changed, 0 insertions, 7 deletions
diff --git a/lib/util.ml b/lib/util.ml index 05b147cee3..429c1666e0 100644 --- a/lib/util.ml +++ b/lib/util.ml @@ -32,12 +32,6 @@ let explode s = let implode sl = String.concat "" sl -let check_is_ident s = - let len = String.length s in - if len = 0 then invalid_arg "parse_loadpath: is not a valid name"; - (* TODO... *) - () - let parse_loadpath s = let len = String.length s in let rec decoupe_dirs n = @@ -46,7 +40,6 @@ let parse_loadpath s = if pos = n then invalid_arg "parse_loadpath: find an empty dir in loadpath"; let dir = String.sub s n (pos-n) in - check_is_ident dir; dir :: (decoupe_dirs (succ pos)) with | Not_found -> [String.sub s n (len-n)] |