From 73cb338ba91642d6f1f7d3d0265d2ab80610627c Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Mon, 14 Dec 2015 14:48:19 +0100 Subject: [PATCH] makefile --- Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Makefile b/Makefile index 4f0e4731..48d9c2fc 100644 --- a/Makefile +++ b/Makefile @@ -129,7 +129,7 @@ devel: make all watch: - while find src/ -print0 | xargs -0 inotifywait -e delete_self -e modify ; do \ + while find src/ benchs/ -print0 | xargs -0 inotifywait -e delete_self -e modify ; do \ echo "============ at `date` ==========" ; \ make ; \ done