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

Allow to set a different `dest_uri` when creating a `File` #3209

Merged

oprypin merged 2 commits into master from desturi

May 8, 2023

Contributor

oprypin commented May 2, 2023

Cache the value of documentation_pages

oprypin force-pushed the desturi branch from c22eedd to 983061e Compare

May 2, 2023 21:51

oprypin added 2 commits

May 7, 2023 17:29


          Allow to set a different dest_uri when creating a File

d5af642


          Cache the value of documentation_pages

4e0429e

oprypin force-pushed the desturi branch from 983061e to 4e0429e Compare

May 7, 2023 15:29

oprypin merged commit 5c9e4dc into master

30 checks passed

oprypin deleted the desturi branch

May 8, 2023 20:14

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment