diff options
| author |  Adam Chlipala <adam@chlipala.net> | 2013-11-21 14:53:01 -0500 |
|---|---|---|
| committer | Adam Chlipala <adam@chlipala.net> | 2013-11-21 14:53:01 -0500 |
| commit | c28405247dd05ecc562e1d7fa46c58e7e42b2a9d (patch) | |
| tree | 0c7462d19746888296663d6aa1a89801c203fb5d /Makefile.in | |
| parent | a889c5a152e7b16f51f31862146d4dabcac4a050 (diff) | |
Experimenting with distribution via 'make dist', to allow deletion of autogenerated files from version control
Diffstat (limited to 'Makefile.in')
| -rw-r--r-- | Makefile.in | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/Makefile.in b/Makefile.in index 760c5bee..4d5a322d 100644 --- a/Makefile.in +++ b/Makefile.in @@ -243,6 +243,7 @@ LIB_UR = $(SRCLIB)/ur LIB_C = $(SRCLIB)/c LIB_JS = $(SRCLIB)/js SUBDIRS = src/c +EXTRA_DIST = demo/* doc/* lib/js/* lib/ur/* src/* src/coq/* xml/* all: all-recursive .SUFFIXES: |