Merge branch '7.5' into 8.4

sebastianbergmann · Oct 25, 2019 · f9f77ec · f9f77ec
2 parents acbc295 + 7be53b7
commit f9f77ec
Showing 1 changed file with 1 addition and 0 deletions.
diff --git a/.gitattributes b/.gitattributes
@@ -1,6 +1,7 @@
 /.docker    export-ignore
 /build      export-ignore
 /tools      export-ignore
+/tools/*    binary
 
 *.php diff=php