lib/Tools/installfonts
changeset 3007 e5efa177ee0c
parent 2784 a78655c814b0
child 3253 ea75747190a7
equal deleted inserted replaced
3006:8a1eb4531fbb 3007:e5efa177ee0c
     1 #!/bin/bash -norc
     1 #!/bin/bash
     2 #
     2 #
     3 # $Id$
     3 # $Id$
     4 #
     4 #
     5 # DESCRIPTION: install the isabelle fonts into your X11 server
     5 # DESCRIPTION: install the isabelle fonts into your X11 server
     6 
     6