Now with the new workflow on github, we need people to review PR to merge in the dev branch. I have push 2 Pull Requests here:
I think this is better that the PR are reviewed for integration by someone different from the the author. So, please have a look to these PRs, discuss and/or merge.
--
Serge Stinckwich
UMI UMMISCO 209 (SU/IRD/UY1)
--
You received this message because you are subscribed to the Google Groups "PolyMath" group.
To unsubscribe from this group and stop receiving emails from it, send an email to
[hidden email].
For more options, visit
https://groups.google.com/d/optout.
Locked
