From 88b98f00facde51bff705a3fb6c32a73937428cb Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Sat, 25 Jul 2009 16:22:17 +0000
Subject: Use Extraction Blacklist

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1114 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 extraction/fixextract | 11 -----------
 1 file changed, 11 deletions(-)

(limited to 'extraction/fixextract')

diff --git a/extraction/fixextract b/extraction/fixextract
index 1ee3c484..86ebdbdd 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
-- 
cgit