Closed xclerc closed 9 years ago
Thanks for this patch... may you split the commit in two, separating the finalize change from the other ones?
Sorry, I did not find how to amend a pull request, and hence created a new one with two commits as requested.
Thanks Xavier!
On Thu, Jan 08, 2015 at 01:52:53AM -0800, Xavier Clerc wrote:
Sorry, I did not find how to amend a pull request, and hence created a new one with two commits as requested.
— Reply to this email directly or view it on GitHub.*
Roberto Di Cosmo
Professeur En delegation a l'INRIA
PPS E-mail: roberto@dicosmo.org
Universite Paris Diderot WWW : http://www.dicosmo.org
Case 7014 Tel : ++33-(0)1-57 27 92 20
5, Rue Thomas Mann
F-75205 Paris Cedex 13 Identica: http://identi.ca/rdicosmo
Attachments: MIME accepted, Word deprecated
Office location:
Bureau 3020 (3rd floor) Batiment Sophie Germain Avenue de France
GPG fingerprint 2931 20CE 3A5A 5390 98EC 8BFC FCCA C3BE 39CB 12D3
The patch is mostly harmless, but one change should be carefully reviewed.
The patch suppresses the 'finalize' parameter from the 'setup_children_chans' function. My understanding is that whenever the function is called in order to create a 'finish' function, a call is also made to 'Pervasives.at_exit' to register 'finalize' to be executed at children termination. It thus seems that the function does not need to be passed 'finalize'.