src/Tools/8bit/doc/Makefile
author nipkow
Tue, 06 May 1997 13:33:33 +0200
changeset 3111 00fb015d27aa
parent 2392 2fb9659d30ca
child 4165 42f2619adfd7
permissions -rw-r--r--
Stupid bug in induct_tac caused warning to always appear.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1826
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
     1
###############################################
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
     2
# Title:      Tools/8bit/doc/Makefile
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
     3
# ID:         $Id$
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
     4
# Author:     David von Oheimb
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
     5
# Copyright   1996 TU Muenchen
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
     6
#
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
     7
# Makefile for the document files
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
     8
###############################################
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
     9
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    10
# operate silently
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    11
MAKEFLAGS='s'
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    12
1907
d069f23e941f Minor improvements of the scripts
oheimb
parents: 1826
diff changeset
    13
LATEX=latex2e
1826
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    14
ISA2LATEX=isa2latex
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    15
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    16
CHECKOUT=co
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    17
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    18
.SUFFIXES: $(SUFFIXES) .itex .thy .ML .tex .dvi
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    19
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    20
.itex.tex:
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    21
	$(ISA2LATEX) -x -e -o $@ $<
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    22
.thy.tex .ML.tex:
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    23
	$(ISA2LATEX) -s -e -f '\oddsidemargin-1cm{}\evensidemargin-1cm' -o $@ $<
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    24
.tex.dvi:
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    25
	$(LATEX) $<
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    26
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    27
FONTDOCFILES = fontindex.dvi keyindex.dvi fkmatrix.dvi
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    28
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    29
fontdocfiles: $(FONTDOCFILES)
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    30
2392
2fb9659d30ca minor adaptions
oheimb
parents: 1907
diff changeset
    31
manual: manual.dvi
1826
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    32
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    33
clean:
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    34
	rm -f *.aux *.log