EXTRA_DIST = man.html