From e5a4502fa68442dad1b771e496b544c6770df751 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Mon, 11 Jul 2005 08:49:03 +0000 Subject: [PATCH] only regular files are ending in .ma are now searched --- helm/matita/library/Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/helm/matita/library/Makefile b/helm/matita/library/Makefile index 5e3aaef45..1a5411c2c 100644 --- a/helm/matita/library/Makefile +++ b/helm/matita/library/Makefile @@ -1,4 +1,4 @@ -SRC=$(shell find . -name "*.ma") +SRC=$(shell find . -name "*.ma" -a -type f) MATITAC=../scripts/do_tests.sh $(DO_TESTS_OPTS) ../matitac ../matitaclean /dev/null MATITACOPT=../scripts/do_tests.sh $(DO_TESTS_OPTS) ../matitac.opt ../matitaclean.opt /dev/null -- 2.39.2