From e77aa73c7499b530c5868bb637c26840afa23c13 Mon Sep 17 00:00:00 2001 From: Guillaume Petiot Date: Thu, 1 Jul 2021 18:00:10 +0800 Subject: [PATCH] forgot js_map.ml.opts --- test/passing/tests/js_map.ml.opts | 1 + 1 file changed, 1 insertion(+) create mode 100644 test/passing/tests/js_map.ml.opts diff --git a/test/passing/tests/js_map.ml.opts b/test/passing/tests/js_map.ml.opts new file mode 100644 index 0000000000..a2f04741b8 --- /dev/null +++ b/test/passing/tests/js_map.ml.opts @@ -0,0 +1 @@ +--max-iter=3