Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Adds make html that does not build the manual as pdf #3620

Merged
merged 1 commit into from
Aug 22, 2019
Merged

Adds make html that does not build the manual as pdf #3620

merged 1 commit into from
Aug 22, 2019

Conversation

DominikBernhardt
Copy link
Contributor

The new version of GAPDoc provides a nodpf option that builds the manual
without generating a .pdf-file.
This PR allows the user to call make html and no .pdf files are created.

This PR is a collaboration with @wilfwilson.
Fixes #3609
Text for release notes:
Adds make html that does not build the manual as pdf

@DominikBernhardt DominikBernhardt added kind: enhancement Label for issues suggesting enhancements; and for pull requests implementing enhancements topic: build system release notes: to be added PRs introducing changes that should be (but have not yet been) mentioned in the release notes labels Aug 22, 2019
@DominikBernhardt DominikBernhardt added the gapsingular2019 Issues and PRs that arose at https://opendreamkit.org/meetings/2019-04-02-GAPSingularMeeting label Aug 22, 2019
Copy link
Member

@wilfwilson wilfwilson left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I wrote the code for this PR so it probably would be right for me to approve it. But I stand by it.

Dominik says that he’s run this on his computer (notably without the already-compiled files present) and he said it worked fine.

@fingolfin fingolfin merged commit f5dfccf into gap-system:master Aug 22, 2019
@coveralls
Copy link

Coverage Status

Coverage remained the same at 84.395% when pulling a42e236 on DominikBernhardt:db/make-html into 1c15c63 on gap-system:master.

@wilfwilson wilfwilson added release notes: added PRs introducing changes that have since been mentioned in the release notes and removed release notes: to be added PRs introducing changes that should be (but have not yet been) mentioned in the release notes labels Aug 26, 2019
@olexandr-konovalov olexandr-konovalov added this to the GAP 4.11.0 milestone Aug 26, 2019
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
gapsingular2019 Issues and PRs that arose at https://opendreamkit.org/meetings/2019-04-02-GAPSingularMeeting kind: enhancement Label for issues suggesting enhancements; and for pull requests implementing enhancements release notes: added PRs introducing changes that have since been mentioned in the release notes topic: build system
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Add make html which builds manuals but w/o PDF
5 participants