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

Missing Travis test for the documentation in pdf #1966

Closed
asr opened this issue May 6, 2016 · 1 comment
Closed

Missing Travis test for the documentation in pdf #1966

asr opened this issue May 6, 2016 · 1 comment
Assignees
Labels
not-in-changelog This issue should not be listed in the changelog. travis (not in changelog) type: enhancement Issues and pull requests about possible improvements ux: documentation Issues relating to Agda's documentation
Milestone

Comments

@asr
Copy link
Member

asr commented May 6, 2016

Blocked by readthedocs/readthedocs.org#1556.

@asr asr self-assigned this May 6, 2016
@asr asr added type: enhancement Issues and pull requests about possible improvements ux: documentation Issues relating to Agda's documentation travis (not in changelog) labels May 6, 2016
@asr asr added this to the 2.5.2 milestone May 6, 2016
@asr asr removed this from the 2.5.2 milestone May 6, 2016
@asr asr added the status: blocked-by-issue This pull request is blocked on an open issue. label Oct 3, 2016
@asr asr closed this as completed in 1719ae3 Jan 9, 2017
@asr asr reopened this Jan 9, 2017
asr referenced this issue Jan 9, 2017
Read the docs fails when using the setting `latex_engine='xelatex'`.
@asr asr removed the status: blocked-by-issue This pull request is blocked on an open issue. label Mar 29, 2018
@asr asr added this to the 2.5.4 milestone Mar 29, 2018
@asr
Copy link
Member Author

asr commented Mar 29, 2018

Fixed by 34087af.

@asr asr closed this as completed Mar 29, 2018
@asr asr added the dev-ops label May 28, 2018
@asr asr added the not-in-changelog This issue should not be listed in the changelog. label Jun 9, 2018
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
not-in-changelog This issue should not be listed in the changelog. travis (not in changelog) type: enhancement Issues and pull requests about possible improvements ux: documentation Issues relating to Agda's documentation
Projects
None yet
Development

No branches or pull requests

1 participant