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 | f2e26534fdc9b02661e00023fbe56d8c4c7c571f (patch) | |
| tree | 0c7462d19746888296663d6aa1a89801c203fb5d /src | |
| parent | 6bbbb54b2b47e3bd14ea71f19fef2da616f91aff (diff) | |
Experimenting with distribution via 'make dist', to allow deletion of autogenerated files from version control
Diffstat (limited to 'src')
0 files changed, 0 insertions, 0 deletions