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

Fix DirectoriesPackagePrograms to ignore case of package name, like LoadPackage does #4035

Merged

Conversation

ThomasBreuer
Copy link
Contributor

DirectoriesPackagePrograms( <name> ) wants to check
whether the package <name> is already available,
but it does not make sure that <name> is in lowercase.
Thus the package may be erroneously regarded as not yet loaded,
and if several versions of the package are installed
then the path for the highest such version is taken,
which may be wrong.

`DirectoriesPackagePrograms( <name> )` wants to check
whether the package `<name>` is already available,
but it does not make sure that `<name>` is in lowercase.
Thus the package may be erroneously regarded as not yet loaded,
and if several versions of the package are installed
then the path for the highest version is taken, which may be wrong.
@ThomasBreuer ThomasBreuer added kind: bug: wrong result Issues describing bugs that result in mathematically or otherwise wrong results, and PRs fixing them topic: packages issues or PRs related to package handling, or specific to a package (for packages w/o issue tracker) release notes: not needed PRs introducing changes that are wholly irrelevant to the release notes labels May 18, 2020
@coveralls
Copy link

Coverage Status

Coverage increased (+0.0003%) to 84.885% when pulling b1ba3c8 on ThomasBreuer:TB_DirectoriesPackagePrograms into b5a0e52 on gap-system:master.

@fingolfin fingolfin merged commit bce3fb4 into gap-system:master May 20, 2020
@fingolfin fingolfin added kind: bug Issues describing general bugs, and PRs fixing them release notes: to be added PRs introducing changes that should be (but have not yet been) mentioned in the release notes and removed release notes: not needed PRs introducing changes that are wholly irrelevant to the release notes labels May 20, 2020
@PaulaHaehndel PaulaHaehndel self-assigned this Feb 16, 2021
@PaulaHaehndel PaulaHaehndel changed the title turn the package name to lowercase normalize package name to all-lowercase in DirectoriesPackagePrograms Feb 16, 2021
@PaulaHaehndel PaulaHaehndel added release notes: added PRs introducing changes that have since been mentioned in the release notes and removed release notes: to be added PRs introducing changes that should be (but have not yet been) mentioned in the release notes labels Feb 16, 2021
@PaulaHaehndel PaulaHaehndel removed their assignment Feb 16, 2021
@fingolfin fingolfin changed the title normalize package name to all-lowercase in DirectoriesPackagePrograms Fix DirectoriesPackagePrograms to ignore case of package name, like LoadPackage does Aug 17, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
kind: bug: wrong result Issues describing bugs that result in mathematically or otherwise wrong results, and PRs fixing them kind: bug Issues describing general bugs, and PRs fixing them release notes: added PRs introducing changes that have since been mentioned in the release notes topic: packages issues or PRs related to package handling, or specific to a package (for packages w/o issue tracker)
Projects
None yet
Development

Successfully merging this pull request may close these issues.

4 participants