diff options
Diffstat (limited to 'Makefile')
| -rw-r--r-- | Makefile | 4 |
1 files changed, 3 insertions, 1 deletions
@@ -6,7 +6,7 @@ # # GNU Lesser General Public License Version 2.1 # ####################################################################### -# $Id: Makefile 11387 2008-09-07 21:59:11Z glondu $ +# $Id: Makefile 11826 2009-01-22 06:43:35Z notin $ # Makefile for Coq @@ -32,6 +32,8 @@ export FIND_VCS_CLAUSE:='(' \ -name 'debian' -or \ -name "$${GIT_DIR}" \ ')' -prune -type f -or +export PRUNE_CHECKER := -wholename ./checker/\* -prune -or + FIND_PRINTF_P:=-print | sed 's|^\./||' export YACCFILES:=$(shell find . $(FIND_VCS_CLAUSE) '(' -name '*.mly' ')' $(FIND_PRINTF_P)) |