No longer needed.

diff --git a/v7/doc/user-manual/re-tex b/v7/doc/user-manual/re-tex
deleted file mode 100755 (executable)
index 10c7e6d..0000000
--- a/v7/doc/user-manual/re-tex
+++ /dev/null
@@ -1,8 +0,0 @@
-#!/bin/sh
-
-tex user.texinfo
-texindex user.cp user.fn user.ky user.pg user.tp user.vr
-tex user.texinfo
-texindex user.cp user.fn user.ky user.pg user.tp user.vr
-tex user.texinfo
-# hopefully by now all the references have reached their correct pages