From 946138ef87372c42faaec413f892115685ddd9f7 Mon Sep 17 00:00:00 2001 From: Felix Cherubini Date: Thu, 8 Feb 2024 16:00:54 +0100 Subject: [PATCH] fix --- GNUmakefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/GNUmakefile b/GNUmakefile index 39b5335528..4d6d8be583 100644 --- a/GNUmakefile +++ b/GNUmakefile @@ -31,7 +31,7 @@ check-whitespace: .PHONY : check-everythings check-everythings: - $(EVERYTHINGS) check-except Experiments + $(EVERYTHINGS) check-except .PHONY : gen-everythings gen-everythings: