redirect make debian as make make -f Makefile.debian
authorThierry Parmentelat <thierry.parmentelat@inria.fr>
Wed, 16 Jan 2013 09:17:22 +0000 (10:17 +0100)
committerThierry Parmentelat <thierry.parmentelat@inria.fr>
Wed, 16 Jan 2013 09:17:22 +0000 (10:17 +0100)
commit312b04f1ac33abb2968fbb4fc6e560fd6a99933b
tree83eff29cb7165ebc6cb23966849694015c19e378
parenta51186605b0699ed12eab88b1663415b3449e5fb
redirect make debian as make make -f Makefile.debian
will make sense to merge both eventually
Makefile