#!/bin/bash
################################################
# Title: Tools/8bit/xmosaic/isa_xmosaic
# ID: $Id$
# Author: Franz Regensburger
# Copyright 1995 TU Muenchen
#
# open xmosaic with isabelle font
#
# Franz Regensburger <regensbu@informatik.tu-muenchen.de> 20.12.95
#
###############################################
#
# The script is configured by the master makefile ../Makefile.
# Edit this file to make changes!
#
###############################################
# do not edit below
###############################################
ISAXMOSAICDIR=$ISABELLE8BIT/xmosaic
# start xmosaic ;
xmosaic -title "isa_xmosaic" -xrm "\
Mosaic*font:isabelle14" -xrm "\
Mosaic*fixedFont:isabelle14" -xrm "\
Mosaic*plainFont:isabelle14"