1 files changed, 0 insertions, 31 deletions
diff --git a/Docs/Support/generate-flag-images b/Docs/Support/generate-flag-images
deleted file mode 100755
index 21140388012..00000000000
--- a/Docs/Support/generate-flag-images
+++ /dev/null
@@ -1,31 +0,0 @@
-#!/bin/sh
-
-flags=`grep @image mirrors.texi | cut -d" " -f1 | cut -d/ -f2 | tr -d "}" | sort | uniq`
-
-set -x
-cd Flags
-
-for c in $flags
-do
-  # For PNM, to be used later
-  giftopnm ../Raw-Flags/$c.gif | pnmscale -xsize 30 > $c-tmp.pnm
-  pnmpaste $c-tmp.pnm 1 1 ../Images/flag-background.pnm > $c.pnm
-  rm -f $c-tmp.pnm
-
-  # For GIF version
-  ppmtogif $c.pnm > $c.gif
-  # or cjpeg -optimize -quality 70 -outfile $c.jpg
-
-  # For EPS version
-  pnmtops -noturn $c.pnm > $c.eps
-
-  # For PDF version
-  ps2pdf $c.eps $c.pdf
-
-  # For text version
-  echo -n "" > $c.txt
-
-  # PNM isn't really needed
-  rm -f $c.pnm
-
-done