From a6eff171bcfc1616b2dbef0fa28b2247230fd74a Mon Sep 17 00:00:00 2001 From: Chris Hanson Date: Mon, 10 Jul 2000 22:05:02 +0000 Subject: [PATCH] No longer needed. --- v7/doc/user-manual/re-tex | 8 -------- 1 file changed, 8 deletions(-) delete mode 100755 v7/doc/user-manual/re-tex diff --git a/v7/doc/user-manual/re-tex b/v7/doc/user-manual/re-tex deleted file mode 100755 index 10c7e6d6d..000000000 --- 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 -- 2.25.1