#!/bin/csh -f

#if ("$cwd" != "$LEDAROOT/Manual/MANUAL") then
#  echo " "
#  echo "must be executed in directory MANUAL"
#  echo " "
#  exit
#endif

if ($1 == "") then
  set source = $LEDAROOT/incl/LEDA
  set dvidir = $LEDAROOT/Manual/DVI
  set ext = h
else 
  set source = $1
  if ($2 == "") then
    set ext = h
  else
    set ext = $2
  endif
endif

rm -r -f $dvidir
mkdir    $dvidir 
cd       $dvidir

echo Making dvi-files for manual pages ...
echo " "

rm -f mkdvi.log

pwd

cp $LEDAROOT/Manual/MANUAL/intro.tex .
cp $LEDAROOT/Manual/MANUAL/Introduction.tex .
cp $LEDAROOT/Manual/MANUAL/Basics.tex .
latex intro.tex 
mv intro.dvi Introduction.dvi
dvips Introduction.dvi

foreach f ($source/*.$ext)
   echo $f
   $LEDAROOT/Manual/cmd/Lman $f xdvi=no dvioutfile=`basename $f .$ext`.dvi >>& mkdvi.log
   dvips `basename $f .$ext`.dvi  >>& mkdvi.log
end

cd ..

