Gentoo Archives: gentoo-commits

From: "Maciej Barć" <xgqt@g.o>
To: gentoo-commits@l.g.o
Subject: [gentoo-commits] repo/gentoo:master commit in: dev-lang/idris2/
Date: Sat, 27 Nov 2021 21:11:11
Message-Id: 1638047459.793a720cdcd065874d2beb7efcad20e208b65bf7.xgqt@gentoo
1 commit: 793a720cdcd065874d2beb7efcad20e208b65bf7
2 Author: Maciej Barć <xgqt <AT> gentoo <DOT> org>
3 AuthorDate: Sat Nov 27 21:10:53 2021 +0000
4 Commit: Maciej Barć <xgqt <AT> gentoo <DOT> org>
5 CommitDate: Sat Nov 27 21:10:59 2021 +0000
6 URL: https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=793a720c
7
8 dev-lang/idris2: use dodoc instead of insinto
9
10 Package-Manager: Portage-3.0.28, Repoman-3.0.3
11 Signed-off-by: Maciej Barć <xgqt <AT> gentoo.org>
12
13 dev-lang/idris2/idris2-0.5.1_p20211112.ebuild | 5 +----
14 1 file changed, 1 insertion(+), 4 deletions(-)
15
16 diff --git a/dev-lang/idris2/idris2-0.5.1_p20211112.ebuild b/dev-lang/idris2/idris2-0.5.1_p20211112.ebuild
17 index 8069d5960163..762d534c28a4 100644
18 --- a/dev-lang/idris2/idris2-0.5.1_p20211112.ebuild
19 +++ b/dev-lang/idris2/idris2-0.5.1_p20211112.ebuild
20 @@ -101,8 +101,5 @@ src_install() {
21 einstalldocs
22
23 # Install documentation
24 - if use doc; then
25 - insinto /usr/share/doc/${PF}/
26 - doins -r ./docs/build/html
27 - fi
28 + use doc && dodoc -r ./docs/build/html
29 }