fix a few disting issues
authorChristian Grothoff <christian@grothoff.org>
Mon, 4 Jun 2018 21:29:34 +0000 (23:29 +0200)
committerChristian Grothoff <christian@grothoff.org>
Mon, 4 Jun 2018 21:29:34 +0000 (23:29 +0200)
commiteec5a96f455942cac2f972f76babfe624849dccc
tree1c4de3daaf98fcb91b9ee8729089bc1e27688363
parent5eb8efafea6d28afb22316e6a51ca9fcabc882cd
fix a few disting issues
contrib/Makefile.am