From 793a720cdcd065874d2beb7efcad20e208b65bf7 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Maciej=20Bar=C4=87?= <xgqt@gentoo.org>
Date: Sat, 27 Nov 2021 22:10:53 +0100
Subject: [PATCH] dev-lang/idris2: use dodoc instead of insinto
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Package-Manager: Portage-3.0.28, Repoman-3.0.3
Signed-off-by: Maciej Barć <xgqt@gentoo.org>
---
 dev-lang/idris2/idris2-0.5.1_p20211112.ebuild | 5 +----
 1 file changed, 1 insertion(+), 4 deletions(-)

diff --git a/dev-lang/idris2/idris2-0.5.1_p20211112.ebuild b/dev-lang/idris2/idris2-0.5.1_p20211112.ebuild
index 8069d59601630..762d534c28a41 100644
--- a/dev-lang/idris2/idris2-0.5.1_p20211112.ebuild
+++ b/dev-lang/idris2/idris2-0.5.1_p20211112.ebuild
@@ -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
 }