summaryrefslogtreecommitdiff
path: root/extraction/fixextract
diff options
context:
space:
mode:
authorGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2009-04-17 13:27:48 +0000
committerGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2009-04-17 13:27:48 +0000
commitd1cdc0496d7d52e3ab91554dbf53fcc0e7f244eb (patch)
tree4fb435a847b0a1f1fd0afc93eb718c459e2aa0d6 /extraction/fixextract
parented39cb168c0ca6c979db9059d39213d4f2a59eb5 (diff)
Various clean-ups
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1033 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'extraction/fixextract')
-rwxr-xr-xextraction/fixextract15
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