Change bin/gap.sh into gap as bin/gap.sh has been removed#26

Merged

fingolfin merged 1 commit intomasterfrom fix-gapname

Nov 29, 2023

+1-1

Commits on Nov 29, 2023

Change bin/gap.sh into gap as bin/gap.sh has been removed
ChrisJefferson
committed