From aafecd5dc3a9dfd92a47fbc5bd4746c0d0d2266b Mon Sep 17 00:00:00 2001
From: Adar Nimrod <nimrod@shore.co.il>
Date: Fri, 1 Jan 2021 20:36:27 +0200
Subject: [PATCH] Clean up the Makefile.

---
 Dockerfile       | 2 +-
 example/Makefile | 5 ++++-
 2 files changed, 5 insertions(+), 2 deletions(-)

diff --git a/Dockerfile b/Dockerfile
index 7c667c0..b69f7f3 100644
--- a/Dockerfile
+++ b/Dockerfile
@@ -43,4 +43,4 @@ WORKDIR /volume
 ENV HOME /volume
 # Run a test build.
 COPY example/ /example/
-RUN make -C /example all clean
+RUN make --debug=j --keep-going -C /example test
diff --git a/example/Makefile b/example/Makefile
index 52561a3..f7e8c09 100644
--- a/example/Makefile
+++ b/example/Makefile
@@ -1,5 +1,7 @@
-.PHONY: all clean
+.PHONY: test
+test: clean all
 
+.PHONY: all
 all: presentation.pdf left-to-right.pdf
 
 presentation.pdf: diagram.pdf
@@ -17,5 +19,6 @@ left-to-right.pdf: left-to-right.md
 %.gif: %.tty
 	ttyrec2gif -in $< -out $@
 
+.PHONY: clean
 clean:
 	- rm *.pdf *.gif
-- 
GitLab