max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore(CMakeLists): remove leftover line

Browse source
This commit is contained in:
Gabriel Ebner 2017-01-05 16:26:30 +01:00 • committed by Leonardo de Moura
parent e8d4af8723
commit 51de81dfd0
1 changed files with 0 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/CMakeLists.txt
View file

@ -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