1 files changed, 9 insertions, 0 deletions
diff --git a/tools/restore-v7 b/tools/restore-v7
new file mode 100755
index 000000000..1115593ed
--- /dev/null
+++ b/tools/restore-v7
@@ -0,0 +1,9 @@
+#!/bin/sh
+
+echo Restoring v7 files from directory v7
+for i in v7/*.v v7/*/*.v v7/*/*/*.v v7/*/*/*/*.v v7/*/*/*/*/*.v v7/*/*/*/*/*/*.v; do
+  if expr $i : '.*\*\.v' > /dev/null ; then continue ; fi
+  j=`echo $i | sed -e "s@^v7/@@"`
+  echo Restoring $i from v7
+  cp -f $i $j
+done