From 9b3419055e9eb7253b6618699e185d06f566cc87 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Mon, 10 Nov 2014 00:49:45 +0100 Subject: [PATCH] stronger inlining for CCVector (so that e.g. push is inline) --- _tags | 1 + 1 file changed, 1 insertion(+) diff --git a/_tags b/_tags index 37a53b13..2026ea27 100644 --- a/_tags +++ b/_tags @@ -160,4 +160,5 @@ : thread : thread : -traverse +: inline(25) <{string,core}/**/*.ml>: warn_A, warn(-4), warn(-44)