diff options
author | Alfredo Tupone <tupone@gentoo.org> | 2022-04-24 10:15:39 +0200 |
---|---|---|
committer | Alfredo Tupone <tupone@gentoo.org> | 2022-04-24 10:15:39 +0200 |
commit | 12e549c395578618fa56e1b3be829692a4a8d11a (patch) | |
tree | f60cb98686f663eb40f996b2c5bec920d55f4b7f /profiles | |
parent | dev-ml/ppx_cold: 0.15.0 bump (diff) | |
download | gentoo-12e549c395578618fa56e1b3be829692a4a8d11a.tar.gz gentoo-12e549c395578618fa56e1b3be829692a4a8d11a.tar.bz2 gentoo-12e549c395578618fa56e1b3be829692a4a8d11a.zip |
package.mask: add ppx_compare to janestreet mask
Signed-off-by: Alfredo Tupone <tupone@gentoo.org>
Diffstat (limited to 'profiles')
-rw-r--r-- | profiles/package.mask | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/profiles/package.mask b/profiles/package.mask index 69b81100629a..01ad232713e6 100644 --- a/profiles/package.mask +++ b/profiles/package.mask @@ -43,6 +43,7 @@ dev-ml/ppx_sexp_conv:0/0.15 dev-ml/stdio:0/0.15.0 dev-ml/parsexp:0/0.15 dev-ml/ppx_cold:0/0.15 +dev-ml/ppx_compare:0/0.15 # Hans de Graaff <graaff@gentoo.org> (2022-04-23) # Obsolete slots that are no longer used by current |