more sensible name develdeb.pkgs as it is used for all debians

[build.git] / config.planetlab / develdeb.pkgs

diff --git a/config.planetlab/develsfa.pkgs b/config.planetlab/develdeb.pkgs
similarity index 100%
rename from config.planetlab/develsfa.pkgs
rename to config.planetlab/develdeb.pkgs