From 9d26b73255b86ec710d8a59c8f196f96229b17c9 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 11 Jan 2006 18:52:41 +0000
Subject: Suppression traducteur

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7846 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tools/restore-v7 | 9 ---------
 1 file changed, 9 deletions(-)
 delete mode 100755 tools/restore-v7

(limited to 'tools/restore-v7')

diff --git a/tools/restore-v7 b/tools/restore-v7
deleted file mode 100755
index ab88458796..0000000000
--- a/tools/restore-v7
+++ /dev/null
@@ -1,9 +0,0 @@
-#!/bin/sh
-
-echo Restoring v7 files from directory v7
-v7files=`find v7 -name \*.v`
-for i in $v7files; do
-  j=`echo $i | sed -e "s@^v7/@@"`
-  echo Restoring $i from v7
-  cp -f $i $j
-done
-- 
cgit v1.2.3