Treat del as label character depending on PHP version

In formatting-preserving pretty printing, treat DEL as a label
character based on the target PHP version (the default of 7.1
imp

Treat del as label character depending on PHP version

In formatting-preserving pretty printing, treat DEL as a label
character based on the target PHP version (the default of 7.1
implying it isn't one).

This avoids failure to round-trip an unchanged input.

show more ...