From 0833ee025dfe21db8ecf6b60aa7ba2a0af43d880 Mon Sep 17 00:00:00 2001 From: kalmarek Date: Thu, 23 Apr 2020 16:48:48 +0200 Subject: [PATCH] remove log redirection --- Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Makefile b/Makefile index 810e345..499f152 100644 --- a/Makefile +++ b/Makefile @@ -31,4 +31,4 @@ groups555: $(GROUPS555) $(GROUPS244) $(GROUPS333) $(GROUPS334) $(GROUPS344) $(GROUPS444) $(GROUPS555): @echo "Checking property (T) for" $@ @mkdir -p log - $(JULIA) --project=. runcomputations.jl $@ &>> log/$@.log + $(JULIA) --project=. runcomputations.jl $@