> Anyway, what is platex? Should it be moved
> to the detection of PPLATEX?
>
> Seems to be a latex variant for dealing with Japanese.
Yes, platex is latex for Japanese.
> Moreover, why configure.py doesn't also check for pdfplatex?
No need for this. pdfplatex is not Japanese pdflatex. We only need to check for latex, platex, and
pdflatex.
> I think that we should only check for the availability of a "latex"
> executable and it is the user responsibility providing scripts
> named "latex" and "pdflatex" which really call the desidered engine.
> Or, better, they could simply change the names in the preferences.
No good idea. Please be aware of the user level - they don't know about these special issues, but
just want to press the DVI and PDF button to get their documents translated. We should check for all
LaTeX executables as we currently do.
regards Uwe