diff --git a/GNUmakefile.in b/GNUmakefile.in index a4f1944278cbffb0b19c27ea8d75a60346c4b59b..f3e7cf824de9e0139370abb5a6b45386bac7dc77 100644 --- a/GNUmakefile.in +++ b/GNUmakefile.in @@ -56,6 +56,7 @@ ifeq ($(EVENTSYS),1) @$(MAKE) -C event post-install endif @$(MAKE) -C mote post-install + @$(MAKE) -C tools post-install # # For installation on the 'ops' or 'users' node (okay, plastic)