make sync won't work onto debian-based deployments (diff. layout)
authorThierry Parmentelat <thierry.parmentelat@inria.fr>
Tue, 22 Jan 2013 10:15:16 +0000 (11:15 +0100)
committerThierry Parmentelat <thierry.parmentelat@inria.fr>
Tue, 22 Jan 2013 10:15:16 +0000 (11:15 +0100)
commit394178168c700cc719ca5d584138d0db02f7d4dd
tree919b0b59591b33841bcda9472fb1bc72f1f2d148
parente07e8e3fe7c447ceacbbf7cd22eba8ae24eb8b1c
make sync won't work onto debian-based deployments (diff. layout)
so use make syncdeb instead
Makefile