Skip to content

Fix file and directory naming#39

Closed
MarekSuchanek wants to merge 4 commits intonextfrom
fix/naming
Closed

Fix file and directory naming#39
MarekSuchanek wants to merge 4 commits intonextfrom
fix/naming

Conversation

@MarekSuchanek
Copy link
Member

@MarekSuchanek MarekSuchanek commented Feb 1, 2026

This must be merged only after #38 and rebasing

As this was really painful fixing due to Git handling of renaming files esp. if the only change is case sensitivity, do not squash this PR as that could break things again.

@MarekSuchanek MarekSuchanek self-assigned this Feb 1, 2026
@MarekSuchanek
Copy link
Member Author

So this cannot be even easily rebased due to handling of case-sensitivity in file names... I will need to rework this again manually, @andresTabiTuwien and @TomMiksa will you be OK with such change or shall we give up on such a rule for consistent file (URL) naming?

@andresTabiTuwien
Copy link
Collaborator

Can we give it up now since Tomek needs it for the deliverable and fix it later?

@MarekSuchanek
Copy link
Member Author

MarekSuchanek commented Feb 2, 2026

Can we give it up now since Tomek needs it for the deliverable and fix it later?

Sure, but URLs will change if file/directory names will change... for example https://docs.ostrails.eu/en/next/tools/FAIR_tools/FAIR-Champion.html becomes https://docs.ostrails.eu/en/next/tools/fair/fair-champion.html 🤷🏻‍♂️ or we can simply give up on this. That is the fastest way. If you are OK with that, feel free to merge changes from next to main (and make a tag if needed).

@andresTabiTuwien
Copy link
Collaborator

I´m OK with it, IDK @TomMiksa ?

@MarekSuchanek
Copy link
Member Author

-> #40

@MarekSuchanek MarekSuchanek deleted the fix/naming branch February 3, 2026 09:01
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants