From bd98852cbd19083ea46a90056666e087f1bb0d67 Mon Sep 17 00:00:00 2001 From: Peter Eisentraut Date: Thu, 9 May 2013 22:21:43 -0400 Subject: [PATCH] Remove make_keywords It is not used anymore. --- src/tools/make_keywords | 15 --------------- 1 file changed, 15 deletions(-) delete mode 100755 src/tools/make_keywords diff --git a/src/tools/make_keywords b/src/tools/make_keywords deleted file mode 100755 index abbbfe000f..0000000000 --- a/src/tools/make_keywords +++ /dev/null @@ -1,15 +0,0 @@ -#!/bin/sh - -# src/tools/make_keywords - -cat </ /'|sed 's/|/\ - /' | sort -b +0 -END