diff --git a/MAKEHELP b/MAKEHELP index 85497e984f87ebc7bbd41eaaa983505b588144fa..c14767f11367de1dac4fbe015ff9202b53b2ef10 100644 --- a/MAKEHELP +++ b/MAKEHELP @@ -25,12 +25,6 @@ Common commands: Shows the targets available in <dir> - make html - make pdf - make ps - - Make documentation - make install Installs GHC, libraries and tools under $(prefix)