From 1240f5a730447e76a348842cc29074fb2c92ca5e Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Wed, 10 Dec 2014 14:30:09 +0100 Subject: [PATCH] use -no-alias-deps --- _tags | 1 + 1 file changed, 1 insertion(+) diff --git a/_tags b/_tags index f9436da1..e3d70cb8 100644 --- a/_tags +++ b/_tags @@ -163,3 +163,4 @@ : -traverse : inline(25) <{string,core}/**/*.ml>: warn_A, warn(-4), warn(-44) +true: no_alias_deps