Hi,
On Thu, Jun 17, 2010 at 02:12:28AM -0400, Bruno C. Mundim wrote:
despite the -P option for the shell built-in 'type' not being present in the the Kubuntu distro GNU bash, version 4.0.33.
The -P option was introduced in bash in version 2.05b. The culprit is most likely not bash, but the ArrangementDocHTML script itself. It specifies /bin/sh as shell, which might be bash but does not have to be bash. Especially new distros replace /bin/sh with a more lightweight shell, e.g. dash.
Has anyone experience on how much we could rely on /bin/bash being present?
On the other hand, you could run something along the following lines to see if htlatex is installed:
which htlatex 2>/dev/null | grep -q htlatex || echo "htlatex not installed"
Frank