# HG changeset patch
# User wenzelm
# Date 1008176590 -3600
# Node ID ff7e534367b5d8ee7937a4571703d02b8764477f
# Parent  8f5e0a335ca75c8e39aad5c11594cca138942f02
obsolete;

diff -r 8f5e0a335ca7 -r ff7e534367b5 lib/Tools/installfonts
--- a/lib/Tools/installfonts	Wed Dec 12 17:43:45 2001 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,81 +0,0 @@
-#!/usr/bin/env bash
-#
-# $Id$
-# Author: Markus Wenzel, TU Muenchen
-# License: GPL (GNU GENERAL PUBLIC LICENSE)
-#
-# DESCRIPTION: install symbol fonts on the current X11 server
-
-
-PRG="$(basename "$0")"
-
-function usage()
-{
-  echo
-  echo "Usage: $PRG [OPTIONS]"
-  echo
-  echo "  Options are:"
-  echo "    -x           install X-Symbol fonts"
-  echo
-  echo "  Install symbol fonts on the current X11 server."
-  echo
-  exit 1
-}
-
-
-## process command line
-
-# options
-
-XSYMB=""
-
-while getopts "x" OPT
-do
-  case "$OPT" in
-    x)
-      XSYMB=true
-      ;;
-    \?)
-      usage
-      ;;
-  esac
-done
-
-shift $(($OPTIND - 1))
-
-
-# args
-
-[ "$#" -ne 0 ] && usage
-
-
-## check fonts
-
-function checkfonts()
-{
-  RESULT=$(xlsfonts -fn "$1" 2>&1) || return 1
-
-  case "$RESULT" in
-    xlsfonts:*)
-      return 1
-      ;;
-  esac
-
-  return 0
-}
-
-
-## main
-
-ISABELLE_PATTERN="-isabelle-fixed-*-isabelle-0"
-XSYMBOL_PATTERN="-xsymb-xsymb0-*"
-
-if [ -z "$XSYMB" ]; then
-  checkfonts "$ISABELLE_PATTERN" || eval $ISABELLE_INSTALLFONTS
-  checkfonts "$ISABELLE_PATTERN" || \
-    echo "Warning: Isabelle fonts probably not installed correctly!" >&2
-else
-  checkfonts "$XSYMBOL_PATTERN" || eval $XSYMBOL_INSTALLFONTS
-  checkfonts "$XSYMBOL_PATTERN" || \
-    echo "Warning: X-Symbol fonts probably not installed correctly!" >&2
-fi