#!/bin/bash

make -f Makefile.old clean
make -f Makefile.old modules
make -f Makefile.old directives

time make html