One more use for String.split_on_char.

master
alainfrisch 2016-07-11 15:23:31 +02:00
parent 7343901e91
commit ae8e0dc352
1 changed files with 1 additions and 7 deletions

View File

@ -510,13 +510,7 @@ let dump_obj ic =
let read_primitive_table ic len =
let p = really_input_string ic len in
let rec split beg cur =
if cur >= len then []
else if p.[cur] = '\000' then
String.sub p beg (cur - beg) :: split (cur + 1) (cur + 1)
else
split beg (cur + 1) in
Array.of_list(split 0 0)
String.split_on_char '\000' p |> List.filter ((<>) "") |> Array.of_list
(* Print an executable file *)