Join GitHub today
GitHub is home to over 31 million developers working together to host and review code, manage projects, and build software together.Sign up
Add 'install-nodoc' target for make #890
@jougs I just sent you a PR adding a required "optional" flag. With this, things work in a way: as long as one only ever calls
I wonder if a complete solution of this problem would require introduction of proper build and install configurations, such as deploy/develop/debug.