From ec751f0d48fa3d6268ed4210d74efac23bc87cbc Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Tue, 2 Oct 2018 04:23:05 +0200
Subject: [tools] Remove unused / obsolete files.

TTBOMK we don't use any of these files since a long time.
---
 tools/check-translate | 23 -----------------------
 1 file changed, 23 deletions(-)
 delete mode 100755 tools/check-translate

(limited to 'tools/check-translate')

diff --git a/tools/check-translate b/tools/check-translate
deleted file mode 100755
index acb6f45903..0000000000
--- a/tools/check-translate
+++ /dev/null
@@ -1,23 +0,0 @@
-#!/bin/sh
-
-echo -------------- Producing translated files ---------------------
-rm */*/*.v8 >& /dev/null
-make COQOPTS=-translate theories || { echo ---- Failed to translate; exit 1; }
-if [ -e translated ]; then rm -r translated; fi
-if [ -e successful-translation ]; then rm -r successful-translation; fi
-if [ -e failed-translation ]; then rm -r failed-translation; fi
-mv theories translated
-mkdir theories
-echo -------------------- Upgrading files --------------------------
-cd translated
-for i in */*.v
-do
-  mkdir ../theories/`dirname $i` >& /dev/null
-  mv "$i"8 ../theories/$i
-done
-cd ..
-echo --------------- Recompiling translated files ------------------
-make theories || { echo ---- Failed to recompile; mv theories failed-translation; mv translated theories; exit 1; }
-echo ----------------- Recompilation successful --------------------
-if [ -e successful-translation ]; then rm -r successful-translation; fi
-mv theories successful-translation; mv translated theories
-- 
cgit v1.2.3