From c06454273b7c91a3b4ffff0ce19796daac3638fc Mon Sep 17 00:00:00 2001 From: Thomas Gazagnaire Date: Wed, 29 Mar 2017 14:22:11 +0200 Subject: [PATCH] miragesdk: add a `dev-clean` target Signed-off-by: Thomas Gazagnaire --- projects/miragesdk/src/Makefile | 3 +++ 1 file changed, 3 insertions(+) diff --git a/projects/miragesdk/src/Makefile b/projects/miragesdk/src/Makefile index 2d97abd86..05bde5710 100644 --- a/projects/miragesdk/src/Makefile +++ b/projects/miragesdk/src/Makefile @@ -65,6 +65,9 @@ clean:: (docker rmi -f $(IMAGE):pkg || echo ok) (docker rmi -f $(IMAGE):dev || echo ok) +dev-clean: + rm -rf _build dhcp-client/calf/_build + dev: cd dhcp-client/calf && mirage configure && make jbuilder build dhcp-client/main.exe