diff options
Diffstat (limited to 'contrib/extraction/test/v2ml.ml')
-rw-r--r-- | contrib/extraction/test/v2ml.ml | 9 |
1 files changed, 0 insertions, 9 deletions
diff --git a/contrib/extraction/test/v2ml.ml b/contrib/extraction/test/v2ml.ml deleted file mode 100644 index 245a1b1e..00000000 --- a/contrib/extraction/test/v2ml.ml +++ /dev/null @@ -1,9 +0,0 @@ -let _ = - for j = 1 to ((Array.length Sys.argv) -1) do - let s = Sys.argv.(j) in - let b = Filename.chop_extension (Filename.basename s) in - let b = String.uncapitalize b in - let d = Filename.dirname s in - print_string (Filename.concat d (b ^ ".ml ")) - done; - print_newline() |