fix(library/hott/Makefile): specify LEAN_OPTIONS "--hott"
This commit is contained in:
parent
9a6df02683
commit
8d4c7b4b2c
1 changed files with 1 additions and 0 deletions
|
@ -1 +1,2 @@
|
||||||
include ../Makefile.common
|
include ../Makefile.common
|
||||||
|
LEAN_OPTIONS+=--hott
|
||||||
|
|
Loading…
Reference in a new issue