Fix Undefined array index thrown by run.php scriptnightly-2019.06.08
commit46c31c336be20cb72d9bf976a6a4b67dddeac2d6
authorYu-Jung Lo <[email protected]>
Fri, 7 Jun 2019 23:45:21 +0000 (7 16:45 -0700)
committerHhvm Bot <[email protected]>
Fri, 7 Jun 2019 23:48:30 +0000 (7 16:48 -0700)
tree7da95b0695fd38825362a6c1154b90ff7f6b54e0
parent47256960d9b7ba48eca0b8d3e9d41a790383f387
Fix Undefined array index thrown by run.php script

Summary: We need to add curly syntax to make sure the array index won't be treated as string when formatting a string literal, otherwise, it may throw OutOfBoundExcpetion since "0" index doesn't exist.

Reviewed By: oulgen, alexeyt

Differential Revision: D15721504

fbshipit-source-id: 2a1880c1b7345822c79da7ac1929e4dcd7ac302f
hphp/test/run.php