diff options
Diffstat (limited to 'extraction/fixextract')
-rwxr-xr-x | extraction/fixextract | 15 |
1 files changed, 15 insertions, 0 deletions
diff --git a/extraction/fixextract b/extraction/fixextract new file mode 100755 index 0000000..1ee3c48 --- /dev/null +++ b/extraction/fixextract @@ -0,0 +1,15 @@ +#!/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 |