Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Don't clean HTML manual if we didn't build it
Clean the HTML manual upon 'maintainer-clean' rather than 'clean' in case it was not built by Make but rather part of the distribution. This is fine even then, as configure will properly require what is needed to build it again if it is missing.
- Loading branch information