mirrors/guru
1
0
Fork 0
mirror of https://github.com/gentoo-mirror/guru.git synced 2026-07-10 15:45:15 -04:00
Code Issues Packages Projects Releases Wiki Activity

dev-lang/lean: exclude style_check test

Browse Source 
Closes: https://bugs.gentoo.org/819093
Package-Manager: Portage-3.0.20, Repoman-3.0.3
Signed-off-by: Maciej Barć <xgqt@riseup.net>
This commit is contained in:
Maciej Barć
2021-10-21 16:13:59 +02:00
parent 56d5f40d5d
commit 46c0040634
2 changed files with 18 additions and 0 deletions
Download Patch File Download Diff File Expand all files Collapse all files

9
dev-lang/lean/lean-3.33.0.ebuild
View File

@@ -41,6 +41,15 @@ src_configure() {
cmake_src_configure
}
src_test() {
local myctestargs=(
# Disable problematic "style_check" cpplint test,
# this also removes python test dependency
--exclude-regex style_check
)
cmake_src_test
}
pkg_postinst() {
elog "You probably want to use lean with mathlib, to install it you can either:"
elog " - Do not install mathlib globally and use local versions"

9
dev-lang/lean/lean-3.34.0.ebuild
View File

@@ -41,6 +41,15 @@ src_configure() {
cmake_src_configure
}
src_test() {
local myctestargs=(
# Disable problematic "style_check" cpplint test,
# this also removes python test dependency
--exclude-regex style_check
)
cmake_src_test
}
pkg_postinst() {
elog "You probably want to use lean with mathlib, to install it you can either:"
elog " - Do not install mathlib globally and use local versions"