From 51de81dfd090d094fdb19d6b9a021c763139ce3c Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Thu, 5 Jan 2017 16:26:30 +0100 Subject: [PATCH] chore(CMakeLists): remove leftover line --- src/CMakeLists.txt | 1 - 1 file changed, 1 deletion(-) diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index e854a8060a..3d7dbdb51e 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -30,7 +30,6 @@ option(IGNORE_SORRY "IGNORE_SORRY" OFF) # When cross-compiling, we do not compile the standard library since # the executable will not work on the host machine option(CROSS_COMPILE "CROSS_COMPILE" OFF) -# When ON we try to minimize the amount of memory needed to compile Lean using gcc. # Include MSYS2 required DLLs and binaries in the binary distribution package option(INCLUDE_MSYS2_DLLS "INCLUDE_MSYS2_DLLS" OFF) # When ON we include githash in the version string