From b0d001669e199f47a7220a3f33b33166f69b9f8b Mon Sep 17 00:00:00 2001 From: Thomas Letan Date: Wed, 5 Feb 2020 21:52:05 +0100 Subject: Make the output of `make` cleaner --- Makefile | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Makefile b/Makefile index 5b95670..3d96f5e 100644 --- a/Makefile +++ b/Makefile @@ -5,8 +5,8 @@ POSTS := $(ORG_POSTS:.org=.html) $(COQ_POSTS:.v=.html) COQCARGS := -async-proofs-cache force build: ${POSTS} - soupault - scripts/update-gitignore.sh ${POSTS} + @soupault + @scripts/update-gitignore.sh ${POSTS} clean: rm -f ${POSTS} -- cgit v1.2.3