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

Change IsPackageLoaded and TestPackage to ignore case of package name, like LoadPackage does #4037

Merged
merged 1 commit into from
May 22, 2020

Conversation

fingolfin
Copy link
Member

No description provided.

@fingolfin fingolfin added kind: bug Issues describing general bugs, and PRs fixing them kind: bug: unexpected error Issues describing bugs in which computation unexpectedly encounters an error, 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: to be added PRs introducing changes that should be (but have not yet been) mentioned in the release notes labels May 20, 2020
For lookup in GAPInfo.PackagesInfo, package names must first
be converted to lowercase.
@fingolfin fingolfin changed the title Fix IsPackageLoaded: must convert package name to lowercase Fix IsPackageLoaded & GAPInfo.PackagesInfo error if the given package name is not normalized to be all-lowercase May 20, 2020
@coveralls
Copy link

Coverage Status

Coverage decreased (-0.0003%) to 84.889% when pulling 5711862 on fingolfin:mh/IsPackageLoaded into bce3fb4 on gap-system:master.

@fingolfin fingolfin merged commit 5fd1809 into gap-system:master May 22, 2020
@fingolfin fingolfin deleted the mh/IsPackageLoaded branch May 22, 2020 14:53
@PaulaHaehndel PaulaHaehndel self-assigned this Feb 16, 2021
@PaulaHaehndel PaulaHaehndel changed the title Fix IsPackageLoaded & GAPInfo.PackagesInfo error if the given package name is not normalized to be all-lowercase normalize package name to all-lowercase in IsPackageLoaded and GAPInfo.PackagesInfo 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 IsPackageLoaded and GAPInfo.PackagesInfo Fix IsPackageLoaded and TestPackage to ignore case of package name, like LoadPackage does Aug 17, 2022
@fingolfin fingolfin changed the title Fix IsPackageLoaded and TestPackage to ignore case of package name, like LoadPackage does Fix IsPackageLoaded and TestPackage to ignore case of package name, like LoadPackage does Aug 17, 2022
@fingolfin fingolfin changed the title Fix IsPackageLoaded and TestPackage to ignore case of package name, like LoadPackage does Change IsPackageLoaded and TestPackage 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: unexpected error Issues describing bugs in which computation unexpectedly encounters an error, 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