In export.cmake, if the detected output format is pdf3, we try to
export to "platex", which usually makes sense, but for this file we
would need to export to "latex". This file is very particular, and
also old, so I do not know if it is worth the time to handle this
case.