diff options
Diffstat (limited to 'extraction/fixextract')
| -rwxr-xr-x | extraction/fixextract | 11 |
1 files changed, 0 insertions, 11 deletions
diff --git a/extraction/fixextract b/extraction/fixextract index 1ee3c48..86ebdbd 100755 --- a/extraction/fixextract +++ b/extraction/fixextract @@ -1,15 +1,4 @@ #!/bin/sh -echo "Fixing file names..." -mv list.ml CoqList.ml -mv list.mli CoqList.mli -mv string.ml CoqString.ml -mv string.mli CoqString.mli -mv int.ml CoqInt.ml -mv int.mli CoqInt.mli - -echo "Conversion List -> CoqList, String -> CoqString, Int -> CoqInt..." -./convert *.mli *.ml - echo "Patching files..." for i in *.patch; do patch < $i; done |