pplatex still used?

[Joost Verburg]

Change tracking now seems to use xcolor for its output, so do we still 
need pplatex (dvipost) in configure.py?

Regards,
Joost