gentoo-mirror/gentoo
1
0
Fork 0
mirror of https://github.com/gentoo-mirror/gentoo.git synced 2026-09-24 04:59:14 -07:00
Code Issues Projects Releases Wiki Activity

dev-lang/idris2: use dodoc instead of insinto

Browse Source 
Package-Manager: Portage-3.0.28, Repoman-3.0.3
Signed-off-by: Maciej Barć <xgqt@gentoo.org>
This commit is contained in:
Maciej Barć
2021-11-27 22:10:53 +01:00
parent 2e6b5def47
commit 793a720cdc
1 changed files with 1 additions and 4 deletions
Download Patch File Download Diff File Expand all files Collapse all files

5
dev-lang/idris2/idris2-0.5.1_p20211112.ebuild
View File

@@ -101,8 +101,5 @@ src_install() {
einstalldocs
# Install documentation
if use doc; then
insinto /usr/share/doc/${PF}/
doins -r ./docs/build/html
fi
use doc && dodoc -r ./docs/build/html
}