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 09:25:03 +0000 (11:25 +0200)
commit350c288773f0038d24ac375a35aeda7b513b4917
tree811955bf430691c05c82519015edd3fdc221fb0a
parent17eba3191b129795cc918893076b1dd5cfe4fb11
use new names when debian building
Makefile.debian