From 6133ffc255c4cfadf93378b93ddd43adf0787120 Mon Sep 17 00:00:00 2001 From: Adam Megacz Date: Sat, 2 Apr 2011 22:53:42 +0000 Subject: [PATCH] fix Makefile bug --- Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Makefile b/Makefile index a691257..97de58b 100644 --- a/Makefile +++ b/Makefile @@ -24,7 +24,7 @@ build/Makefile.coq: $(coqfiles) src/categories/src src/categories/src: git submodule update --init src/categories - cd compiler/categories; git checkout master + cd src/categories; git checkout master clean: rm -rf build -- 1.7.10.4