Skip to content

Remove double docs/docs in edit links on jline.org (fixes #1309)#1310

Merged
gnodet merged 1 commit into
jline:masterfrom
vorburger:patch-11
Jul 4, 2025
Merged

Remove double docs/docs in edit links on jline.org (fixes #1309)#1310
gnodet merged 1 commit into
jline:masterfrom
vorburger:patch-11

Conversation

@vorburger
Copy link
Copy Markdown
Contributor

Fixes #1309 ... hopefully. I have to admit that I have not actually taken the time to myself locally run https://docusaurus.io to verify that this indeed does the trick. But it looks about right? 🤣

@gnodet gnodet added the chore label May 29, 2025
@gnodet gnodet added this to the 3.30.5 milestone May 29, 2025
@gnodet gnodet merged commit df2e04a into jline:master Jul 4, 2025
9 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Edit button on https://jline.org documentation website has link to wrong GitHub MD source due to double /docs/docs/

2 participants