From 75a6259813c1476e926454728c9b32fc324b8a7f Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Thu, 6 Apr 2017 17:02:34 -0400
Subject: Ladderstep isn't *that* heavy

---
 Makefile | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'Makefile')

diff --git a/Makefile b/Makefile
index a2c33ed49..9ecc8674d 100644
--- a/Makefile
+++ b/Makefile
@@ -44,7 +44,7 @@ UNMADE_VOFILES := src/SpecificGen/% src/Specific/%Display.vo
 # targets by the "lite" target
 # N.B. if a file not in this list depends on one in this list,
 # that file will be built by the "lite" target
-HEAVY_VOFILES := src/WeierstrassCurve/WeierstrassCurveTheorems.vo src/Specific/IntegrationTestLadderstep.vo
+HEAVY_VOFILES := src/WeierstrassCurve/WeierstrassCurveTheorems.vo # src/Specific/IntegrationTestLadderstep.vo
 
 COQ_VOFILES := $(filter-out $(UNMADE_VOFILES),$(VOFILES))
 LITE_VOFILES := $(filter-out $(HEAVY_VOFILES),$(COQ_VOFILES))
-- 
cgit v1.2.3