From 8d4c7b4b2c2390c8fc726d065909a02a3eff4a4a Mon Sep 17 00:00:00 2001
From: Soonho Kong <soonhok@cs.cmu.edu>
Date: Wed, 6 Aug 2014 17:38:30 -0700
Subject: [PATCH] fix(library/hott/Makefile): specify LEAN_OPTIONS "--hott"

---
 library/hott/Makefile | 1 +
 1 file changed, 1 insertion(+)

diff --git a/library/hott/Makefile b/library/hott/Makefile
index 0a42375f1..20770a207 100644
--- a/library/hott/Makefile
+++ b/library/hott/Makefile
@@ -1 +1,2 @@
 include ../Makefile.common
+LEAN_OPTIONS+=--hott