From f299ce6d76c4a5ab937583fb4f1468216e1524b0 Mon Sep 17 00:00:00 2001 From: regnat Date: Wed, 19 Apr 2017 09:25:48 +0200 Subject: [PATCH] fix makefile main target --- Makefile | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/Makefile b/Makefile index 32b6306..cd9685e 100644 --- a/Makefile +++ b/Makefile @@ -3,8 +3,7 @@ .PHONY: all clean -all: grammar/grammar.pdf semantics/semantics.pdf typing/records.pdf \ - typing/type-system.pdf +all: combined/main.pdf %.pdf: %.tex common/header.tex FORCE latexmk -output-directory=out -pdf -xelatex -pv -use-make $<