[dune-pdelab] pdelab howto does not build

[Markus Blatt]

Hi,

I have problems building the pdelab-howto, can anyone confirm this?

make[3]: Entering directory
`/home/mblatt/src/dune/current/dune-pdelab-howto/doc/howto'
set -e; builddir=$PWD; \
    pushd .; latex -output-directory=$builddir </dev/null
    pdelab-howto-article; popd; \
    while grep Rerun pdelab-howto-article.log > /dev/null ; do \
      pushd .; latex -output-directory=$builddir </dev/null
      pdelab-howto-article; popd; \
      done; \
      if grep '^\\bibdata{' *.aux > /dev/null \
         && grep '^\\citation{' *.aux > /dev/null; \
	 then \
	   BSTINPUTS=.:.:: BIBINPUTS=.:.:: bibtex pdelab-howto-article
	   || exit $?; \
	     pushd .; latex -output-directory=$builddir </dev/null
	     pdelab-howto-article; popd; \
	       while grep Rerun pdelab-howto-article.log > /dev/null ;
	       do \
	           pushd .; latex -output-directory=$builddir
		   </dev/null pdelab-howto-article; popd; \
		     done ; \
		     fi
/bin/sh: pushd: not found
make[3]: *** [pdelab-howto-article.dvi] Fehler 127


It seems like pushd is specific to bash and not available in sh.

Markus