diff options
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 40a4899d6b98..e38f6c22af6a 100644 --- a/profiles/package.mask +++ b/profiles/package.mask @@ -34,6 +34,7 @@ # Breaks some of its rev deps, still in beta stage >=dev-lang/ocaml-4.03_beta >=dev-ml/camlp4-4.03 +>=dev-ml/ppx_tools-0.99.3_p20160217 # Lars Wendler <polynomial-c@gentoo.org> (01 Mar 2016) # Arrow keys don't work (bug #576086). |