Merge branch 'PHP-7.2' into PHP-7.3

diff --cc NEWS
index b86eca4a8b3f9df7b44b01cc2880d84133246b6a,967fed2918ad412d54f4372cac79142b6c30d48c..1c4d7ce14b3e0316de3a58d59ec1342e88b8e31e
--- 1/NEWS
--- 2/NEWS
+++ b/NEWS
@@@ -31,8 -37,10 +31,10 @@@ PH
      custom wrapper). (Laruence)
    . Fixed bug #77669 (Crash in extract() when overwriting extracted array).
      (Nikita)
+   . Fixed bug #76717 (var_export() does not create a parsable value for
+     PHP_INT_MIN). (Nikita)
  
 -07 Mar 2019, PHP 7.2.16
 +07 Mar 2019, PHP 7.3.3
  
  - Core:
    . Fixed bug #77589 (Core dump using parse_ini_string with numeric sections).

diff --cc ext/standard/var.c
Simple merge