use new names when debian building
authorThierry Parmentelat <thierry.parmentelat@inria.fr>
Thu, 2 May 2013 09:25:03 +0000 (11:25 +0200)
committerThierry Parmentelat <thierry.parmentelat@inria.fr>
Thu, 2 May 2013 10:58:49 +0000 (12:58 +0200)
commit93c25a1b2bf8f9dd614e6d8946d0d02c1925ab4f
tree5f38184e0fcec89affb47a0f151da85e4a3688b7
parent9fbdce428012b34b4d9ebd2247e3eb2614d6e8a7
use new names when debian building
Makefile.debian