Browse Source

Include `dev/rename.*' in the distribution.

Ludovic Courtès 13 years ago
parent
commit
07aaeb4d78
1 changed files with 4 additions and 0 deletions
  1. 4 0
      tools/Makefile.am

+ 4 - 0
tools/Makefile.am

@@ -25,6 +25,10 @@ dist_bin_SCRIPTS =
 
 dist_pkgdata_DATA = gdbinit
 
+EXTRA_DIST =					\
+  dev/rename.sed				\
+  dev/rename.sh
+
 CLEANFILES = *.gcno *.gcda *.linkinfo
 
 bin_PROGRAMS += starpu_calibrate_bus