Merge branch 'main' into pr/2021-11/Reservoir_sampling

sanmai · Jan 15, 2022 · 72b7d66 · 72b7d66
2 parents 36e4352 + c74636c
commit 72b7d66
Show file tree

Hide file tree

Showing 2 changed files with 1 addition and 4 deletions.
diff --git a/Makefile b/Makefile
@@ -24,7 +24,7 @@ export XDEBUG_MODE=coverage
 
 # Phan
 PHAN=vendor/bin/phan
-PHAN_ARGS=-j $(JOBS)
+PHAN_ARGS=-j $(JOBS) --allow-polyfill-parser
 PHAN_PHP_VERSION=7.1
 export PHAN_DISABLE_XDEBUG_WARN=1
 

diff --git a/infection.json.dist b/infection.json.dist
@@ -9,8 +9,5 @@
         "@default": true,
         "IdenticalEqual": false,
         "NotIdenticalNotEqual": false
-    },
-    "logs": {
-        "badge": {"branch": "main"}
     }
 }