Merge branch 'jit' of ssh://git.nguyen.vg/tatoo into jit jit
authorKim Nguyễn <kim.nguyen@lri.fr>
Tue, 18 Apr 2017 12:53:58 +0000 (14:53 +0200)
committerKim Nguyễn <kim.nguyen@lri.fr>
Tue, 18 Apr 2017 12:53:58 +0000 (14:53 +0200)

Trivial merge