|
1826
|
1 |
#!/bin/bash
|
|
|
2 |
################################################
|
|
|
3 |
# Title: Tools/8bit/xmosaic/isa_xmosaic
|
|
|
4 |
# ID: $Id$
|
|
|
5 |
# Author: Franz Regensburger
|
|
|
6 |
# Copyright 1995 TU Muenchen
|
|
|
7 |
#
|
|
|
8 |
# open xmosaic with isabelle font
|
|
|
9 |
#
|
|
|
10 |
# Franz Regensburger <regensbu@informatik.tu-muenchen.de> 20.12.95
|
|
|
11 |
#
|
|
|
12 |
###############################################
|
|
|
13 |
#
|
|
|
14 |
# The script is configured by the master makefile ../Makefile.
|
|
|
15 |
# Edit this file to make changes!
|
|
|
16 |
#
|
|
|
17 |
|
|
|
18 |
###############################################
|
|
|
19 |
# do not edit below
|
|
|
20 |
###############################################
|
|
|
21 |
|
|
|
22 |
ISAXMOSAICDIR=$ISABELLE8BIT/xmosaic
|
|
|
23 |
|
|
|
24 |
# start xmosaic ;
|
|
|
25 |
|
|
|
26 |
xmosaic -title "isa_xmosaic" -xrm "\
|
|
2852
|
27 |
Mosaic*font:isabelle14" -xrm "\
|
|
|
28 |
Mosaic*fixedFont:isabelle14" -xrm "\
|
|
|
29 |
Mosaic*plainFont:isabelle14"
|