src/Tools/8bit/doc/Makefile
author paulson
Tue, 16 Jul 1996 15:49:46 +0200
changeset 1868 836950047d85
parent 1826 2a2c0dbeb4ac
child 1907 d069f23e941f
permissions -rw-r--r--
Put in minimal simpset to avoid excessive simplification, just as in revision 1.9 of HOL/indrule.ML

###############################################
# Title:      Tools/8bit/doc/Makefile
# ID:         $Id$
# Author:     David von Oheimb
# Copyright   1996 TU Muenchen
#
# Makefile for the document files
###############################################

# operate silently
MAKEFLAGS='s'

LATEX=latex
ISA2LATEX=isa2latex

CHECKOUT=co

.SUFFIXES: $(SUFFIXES) .itex .thy .ML .tex .dvi

.itex.tex:
	$(ISA2LATEX) -x -e -o $@ $<
.thy.tex .ML.tex:
	$(ISA2LATEX) -s -e -f '\oddsidemargin-1cm{}\evensidemargin-1cm' -o $@ $<
.tex.dvi:
	$(LATEX) $<

FONTDOCFILES = fontindex.dvi keyindex.dvi fkmatrix.dvi

fontdocfiles: $(FONTDOCFILES)

manual: manual.tex manual.dvi

manual.tex: manual.itex

clean:
	rm -f *.aux *.log