From 670bfe24f565b1c2d5cdb6528112d173c9a1a9ab Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 15 Aug 2014 13:30:56 -0700
Subject: [PATCH] chore(build): remove hott library directory, and move hott
 tests

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 library/hott/Makefile             | 2 --
 src/shell/CMakeLists.txt          | 9 ---------
 tests/lean/{hott => run}/uuu.lean | 0
 3 files changed, 11 deletions(-)
 delete mode 100644 library/hott/Makefile
 rename tests/lean/{hott => run}/uuu.lean (100%)

diff --git a/library/hott/Makefile b/library/hott/Makefile
deleted file mode 100644
index 20770a207..000000000
--- a/library/hott/Makefile
+++ /dev/null
@@ -1,2 +0,0 @@
-include ../Makefile.common
-LEAN_OPTIONS+=--hott
diff --git a/src/shell/CMakeLists.txt b/src/shell/CMakeLists.txt
index 6cabe00f8..78400443a 100644
--- a/src/shell/CMakeLists.txt
+++ b/src/shell/CMakeLists.txt
@@ -75,15 +75,6 @@ FOREACH(T ${LEANSLOWTESTS})
   set_tests_properties("leanslowtest_${T_NAME}" PROPERTIES LABELS "expensive")
 ENDFOREACH(T)
 
-# LEAN HoTT TESTS
-file(GLOB LEANHOTTTESTS "${LEAN_SOURCE_DIR}/../tests/lean/hott/*.lean")
-FOREACH(T ${LEANHOTTTESTS})
-  GET_FILENAME_COMPONENT(T_NAME ${T} NAME)
-  add_test(NAME "leanhotttest_${T_NAME}"
-           WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/hott"
-           COMMAND "./test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean" ${T_NAME})
-ENDFOREACH(T)
-
 # LEAN LUA TESTS
 file(GLOB LEANLUATESTS "${LEAN_SOURCE_DIR}/../tests/lua/*.lua")
 FOREACH(T ${LEANLUATESTS})
diff --git a/tests/lean/hott/uuu.lean b/tests/lean/run/uuu.lean
similarity index 100%
rename from tests/lean/hott/uuu.lean
rename to tests/lean/run/uuu.lean