search

gap-packages / io

GAP package IO to do input and output
https://gap-packages.github.io/io/
Other
14 stars 14 forks source link

Don't wait for child processes to exit on GAP exit #34

Closed ChrisJefferson closed 8 years ago

ChrisJefferson commented 9 years ago

ping

olexandr-konovalov commented 9 years ago

No description provided - could you add perhaps some more details to speed up reviewing this?

ChrisJefferson commented 9 years ago

After a change a couple of versions ago, IO will wait for all child processes to exit before GAP exits, mainly to ensure all pipes are flushed. This lead to the problem that if you have a child process which doesn't exit, GAP hangs.

This patch makes us flush all pipes, but not wait for child processes to finish.

It might be better to try to tidy up, but that would be a further, bigger change.