summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorAlfredo Tupone <tupone@gentoo.org>2022-04-24 13:30:09 +0200
committerAlfredo Tupone <tupone@gentoo.org>2022-04-24 13:30:09 +0200
commit6b6aefb2ef176b2538468e534e769b3ea069bd5f (patch)
tree2943f53b9accdb99894f5df00f88515d8d6d199e /profiles/package.mask
parentdev-java/jrobin: removed obsolete 1.6.0-r1 (diff)
downloadgentoo-6b6aefb2ef176b2538468e534e769b3ea069bd5f.tar.gz
gentoo-6b6aefb2ef176b2538468e534e769b3ea069bd5f.tar.bz2
gentoo-6b6aefb2ef176b2538468e534e769b3ea069bd5f.zip
package.mask: add ppx_here to janestreet mask
Signed-off-by: Alfredo Tupone <tupone@gentoo.org>
Diffstat (limited to 'profiles/package.mask')
-rw-r--r--profiles/package.mask1
1 files changed, 1 insertions, 0 deletions
diff --git a/profiles/package.mask b/profiles/package.mask
index a470ac0b366e..3ffd6634a025 100644
--- a/profiles/package.mask
+++ b/profiles/package.mask
@@ -47,6 +47,7 @@ dev-ml/parsexp:0/0.15
dev-ml/ppx_base:0/0.15
#dev-ml/fieldslib
dev-ml/ppx_fields_conv:0/0.15
+dev-ml/ppx_here:0/0.15
dev-ml/ppx_inline_test:0/0.15.0
dev-ml/ppx_expect:0/0.15.0