Closed stefanoconti closed 5 years ago
@stefanoconti I merged your contribute in devel.
devel
The PR will be marked as closed once devel will be merged in master. This is because I merged "by hand" your PR (a git rebase was needed) and GitHub parse commit keywords only if in master.
master
git rebase
Thanks for your contribution!
@stefanoconti I merged your contribute in
devel.The PR will be marked as closed once
develwill be merged inmaster. This is because I merged "by hand" your PR (agit rebasewas needed) and GitHub parse commit keywords only if inmaster.Thanks for your contribution!