diff options
author | Samuel Mimram <smimram@debian.org> | 2008-07-25 15:12:53 +0200 |
---|---|---|
committer | Samuel Mimram <smimram@debian.org> | 2008-07-25 15:12:53 +0200 |
commit | a0cfa4f118023d35b767a999d5a2ac4b082857b4 (patch) | |
tree | dabcac548e299fee1da464c93b3dba98484f45b1 /contrib/extraction/test/ml2v.ml | |
parent | 2281410e38ef99d025ea77194585a9bc019fdaa9 (diff) |
Imported Upstream version 8.2~beta3+dfsgupstream/8.2.beta3+dfsg
Diffstat (limited to 'contrib/extraction/test/ml2v.ml')
-rw-r--r-- | contrib/extraction/test/ml2v.ml | 14 |
1 files changed, 0 insertions, 14 deletions
diff --git a/contrib/extraction/test/ml2v.ml b/contrib/extraction/test/ml2v.ml deleted file mode 100644 index 363ea642..00000000 --- a/contrib/extraction/test/ml2v.ml +++ /dev/null @@ -1,14 +0,0 @@ -let _ = - 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_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_string fv - done; - print_newline() |