# HG changeset patch
# User wenzelm
# Date 848334479 -3600
# Node ID e8271379ba4b161f595e0cbbd0a619d61cbf5763
# Parent  63a68a3a8a768d42fbe3bb01e43d51c18d4b38d9
added Syntax/symbol_font.ML;

diff -r 63a68a3a8a76 -r e8271379ba4b src/Pure/Makefile
--- a/src/Pure/Makefile	Mon Nov 18 16:34:37 1996 +0100
+++ b/src/Pure/Makefile	Mon Nov 18 17:27:59 1996 +0100
@@ -30,7 +30,7 @@
 SYNTAX_FILES =	Syntax/ROOT.ML	Syntax/ast.ML		Syntax/lexicon.ML\
 	Syntax/parser.ML	Syntax/type_ext.ML	Syntax/syn_trans.ML\
 	Syntax/pretty.ML	Syntax/printer.ML	Syntax/syntax.ML\
-	Syntax/syn_ext.ML	Syntax/mixfix.ML
+	Syntax/syn_ext.ML	Syntax/mixfix.ML	Syntax/symbol_font.ML
 
 THY_FILES = Thy/ROOT.ML		Thy/thy_scan.ML		Thy/thy_parse.ML\
 	Thy/thy_syn.ML		Thy/thy_read.ML		Thy/thm_database.ML