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.

Sign up for GitHub

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

Jump to bottom

Use IOCapture instead of withoutput #124

Merged
merged 9 commits into from
Mar 16, 2021
Merged

Use IOCapture instead of withoutput #124

merged 9 commits into from
Mar 16, 2021

Conversation

mortenpi
Copy link
Contributor

To reduce code duplication 🙂

mortenpi
mortenpi commented Oct 25, 2020
View reviewed changes
src/Literate.jl Outdated Show resolved Hide resolved
@fredrikekre fredrikekre mentioned this pull request Mar 12, 2021
Closed
@mortenpi
Copy link
Contributor Author

mortenpi commented Mar 14, 2021 •
edited
Loading

This should be good to go now. Actually, scratch that -- this downgrades Documenter at the moment because Documenter still uses IOCapture v0.1.

@mortenpi mortenpi mentioned this pull request Mar 14, 2021
Merged
@mortenpi
Copy link
Contributor Author

I updated docs/Manifest.toml to use Documenter#master. Do you have any objections to building the docs with that version for a while?

@fredrikekre
Copy link
Owner

No, but needs #135 too. Can you cherry pick that to this branch maybe?

@mortenpi
Use explicit deploy config object
9c01868 
(cherry picked from commit e3a9e56)

Close fredrikekre#135.
@mortenpi
Copy link
Contributor Author

Good point. Done.

@mortenpi
Copy link
Contributor Author

The documentation failure should be fine -- it's the preview trying to deploy but erroring because it's a PR (which makes deploydocs throw an error since JuliaDocs/Documenter.jl#1529 was merged).

@fredrikekre
Copy link
Owner

But why did it come as far as trying to push in the first place?

@fredrikekre fredrikekre merged commit de9a8a2 into fredrikekre:master Mar 16, 2021
@mortenpi
Copy link
Contributor Author

It checks for GITHUB_TOKEN, which exists, but doesn't have write permissions.

@fredrikekre
Copy link
Owner

Hmm okay. I guess Documenter should be fixed to make sure the PR is from a branch in the same repo or something?

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
2 participants
@mortenpi @fredrikekre