From cf9b021adcc01ac1bbcb3f63300875e9d5ed6e01 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Tue, 3 Jan 2023 16:21:16 +0100 Subject: [PATCH] fix make clean --- Makefile | 1 - 1 file changed, 1 deletion(-) diff --git a/Makefile b/Makefile index b545494d3..17adac1a3 100644 --- a/Makefile +++ b/Makefile @@ -98,7 +98,6 @@ clean: lpoclean @dune clean @$(MAKE) -C editors/emacs clean @$(MAKE) -C editors/vscode clean - @$(MAKE) -C Logic clean .PHONY: distclean distclean: clean