@@ -1,5 +1,5 @@
saved_pwd_before_making=$PWD
-for file in `find example tools -name Makefile`; do
+for file in `find tools example -name Makefile`; do
cd $(dirname $file)
echo
echo "[$file]"