Commit 6e11a11d5508193648c42da4590ef247fc79a1d5

Bruno Haible 2016-12-30T01:15:54

Make Makefile.devel consistent with .gitignore.