make doc stays stuck in gap + fix

gap-packages / io

GAP package IO to do input and output

https://gap-packages.github.io/io/

Other

14 stars 14 forks source link

Closed jgmbenoit closed 1 year ago

jgmbenoit commented 3 years ago

My guess is that a terminal quit; is missing in makedoc.g. hth, Jerome

fingolfin commented 1 year ago

Dang, I missed this issue, so sorry :-(.

Even more annoying as this is really a bug in Makefile.gappkg, and it affects several other packages. Will work on a fix.