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

sci-mathematics/lean-mathlib: fix doc install

Browse Source 
Signed-off-by: Alessandro Barbieri <lssndrbarbieri@gmail.com>
This commit is contained in:
Alessandro Barbieri
2021-10-23 07:11:22 +02:00
parent 09a98b0cd3
commit 88ff538278
1 changed files with 1 additions and 1 deletions
Download Patch File Download Diff File Expand all files Collapse all files

2
sci-mathematics/lean-mathlib/lean-mathlib-0.1_p20211021.ebuild
View File

@@ -32,7 +32,7 @@ src_compile() {
}
src_install() {
dodoc -r docs
dodoc -r docs/*
rm -r docs || die
insinto /usr/lib/lean/mathlib
doins -r .