summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorMaciej Barć <xgqt@gentoo.org>2022-02-22 19:32:10 +0100
committerMaciej Barć <xgqt@gentoo.org>2022-02-22 19:34:04 +0100
commit024840070aea8eb50149f8f9d97df53a3f1fb940 (patch)
tree3d12a992db913f07148cfb090a5e23377c39e8f1 /sci-mathematics/lean/lean-3.9999.ebuild
parentsci-mathematics/lean: drop old 3.37.0 (diff)
downloadgentoo-024840070aea8eb50149f8f9d97df53a3f1fb940.tar.gz
gentoo-024840070aea8eb50149f8f9d97df53a3f1fb940.tar.bz2
gentoo-024840070aea8eb50149f8f9d97df53a3f1fb940.zip
sci-mathematics/lean: remove USE=json and inherit of optfeature
Closes: https://bugs.gentoo.org/833900 Package-Manager: Portage-3.0.30, Repoman-3.0.3 Signed-off-by: Maciej Barć <xgqt@gentoo.org>
Diffstat (limited to 'sci-mathematics/lean/lean-3.9999.ebuild')
-rw-r--r--sci-mathematics/lean/lean-3.9999.ebuild8
1 files changed, 4 insertions, 4 deletions
diff --git a/sci-mathematics/lean/lean-3.9999.ebuild b/sci-mathematics/lean/lean-3.9999.ebuild
index a15591b790f5..5d8ee8eecd4b 100644
--- a/sci-mathematics/lean/lean-3.9999.ebuild
+++ b/sci-mathematics/lean/lean-3.9999.ebuild
@@ -1,4 +1,4 @@
-# Copyright 1999-2021 Gentoo Authors
+# Copyright 1999-2022 Gentoo Authors
# Distributed under the terms of the GNU General Public License v2
EAPI=8
@@ -6,7 +6,7 @@ EAPI=8
MAJOR=$(ver_cut 1)
CMAKE_IN_SOURCE_BUILD="ON"
-inherit cmake optfeature readme.gentoo-r1
+inherit cmake readme.gentoo-r1
DESCRIPTION="The Lean Theorem Prover"
HOMEPAGE="https://leanprover-community.github.io/"
@@ -22,7 +22,7 @@ S="${WORKDIR}/lean-${PV}/src"
LICENSE="Apache-2.0"
SLOT="0/${MAJOR}"
-IUSE="debug +json +threads"
+IUSE="debug +threads"
RDEPEND="dev-libs/gmp:="
DEPEND="${RDEPEND}"
@@ -40,7 +40,7 @@ src_configure() {
local mycmakeargs=(
-DALPHA=ON
-DAUTO_THREAD_FINALIZATION=ON
- -DJSON=$(usex json)
+ -DJSON=ON # bug 833900
-DLEAN_EXTRA_CXX_FLAGS="${CXXFLAGS}"
-DMULTI_THREAD=$(usex threads)
-DUSE_GITHASH=OFF