diff options
Diffstat (limited to 'contrib/extraction/test/ml2v.ml')
| -rw-r--r-- | contrib/extraction/test/ml2v.ml | 13 |
1 files changed, 7 insertions, 6 deletions
diff --git a/contrib/extraction/test/ml2v.ml b/contrib/extraction/test/ml2v.ml index 2cf9190e1..363ea642f 100644 --- a/contrib/extraction/test/ml2v.ml +++ b/contrib/extraction/test/ml2v.ml @@ -1,13 +1,14 @@ let _ = - let j = Array.length Sys.argv in - if j > 0 then - let fml = Sys.argv.(1) in + for j = 1 to ((Array.length Sys.argv)-1) do + let fml = Sys.argv.(j) in let f = Filename.chop_extension fml in let fv = f ^ ".v" in if Sys.file_exists ("../../../" ^ fv) then - print_endline fv + print_string (fv^" ") else let d = Filename.dirname f in let b = String.capitalize (Filename.basename f) in - let fv = Filename.concat d (b ^ ".v") in - print_endline fv + let fv = Filename.concat d (b ^ ".v ") in + print_string fv + done; + print_newline() |