diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2009-07-25 16:22:17 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2009-07-25 16:22:17 +0000 |
commit | 88b98f00facde51bff705a3fb6c32a73937428cb (patch) | |
tree | c6ddc1be5a9790044e0380a15fa6b48e60cc7acc /extraction/fixextract | |
parent | 6c22a0fe2545bf65acdbd067aea25f6e1b96a7cd (diff) |
Use Extraction Blacklist
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1114 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
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 |