diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-04-06 17:02:34 -0400 |
|---|---|---|
| committer |  Jason Gross <jasongross9@gmail.com> | 2017-04-07 13:36:36 -0400 |
| commit | 75a6259813c1476e926454728c9b32fc324b8a7f (patch) | |
| tree | cb09657fceda014aae772f5142e9e0ee5a49e1a0 /Makefile | |
| parent | 500c79d80a2126a8d94347d7c23d4d3423d364b0 (diff) | |
Ladderstep isn't *that* heavy
Diffstat (limited to 'Makefile')
| -rw-r--r-- | Makefile | 2 |
1 files changed, 1 insertions, 1 deletions
@@ -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)) |