diff options
Diffstat (limited to 'Makefile.am')
| -rw-r--r-- | Makefile.am | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/Makefile.am b/Makefile.am index 3b7fa88d..0cd94747 100644 --- a/Makefile.am +++ b/Makefile.am @@ -114,3 +114,5 @@ reauto: libtoolize -cf automake --add-missing --force-missing --copy autoreconf + +EXTRA_DIST = demo/* doc/* lib/js/* lib/ur/* src/* src/coq/* xml/* |