diff options
| author | Enrico Tassi | 2018-04-20 11:08:59 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2018-04-20 11:08:59 +0200 |
| commit | b78523ff2c3349e98686871891028069edfa7523 (patch) | |
| tree | c3ca48d343ea1562e04c1614ff97abeda5d5619e /etc/Makefile | |
| parent | ed05182cece6bb3706e09b2ce14af4a41a2e8141 (diff) | |
move etc/ files to the root and remove obsolete ones
Diffstat (limited to 'etc/Makefile')
| -rw-r--r-- | etc/Makefile | 6 |
1 files changed, 0 insertions, 6 deletions
diff --git a/etc/Makefile b/etc/Makefile deleted file mode 100644 index 5515da0..0000000 --- a/etc/Makefile +++ /dev/null @@ -1,6 +0,0 @@ -VERSION=$(shell git symbolic-ref --short HEAD | cut -d / -f 2) - -dist: - cd ..; git archive --format tar --prefix mathcomp-$(VERSION)/\ - -o mathcomp-$(VERSION).tar HEAD - cd ..; gzip -f -9 mathcomp-$(VERSION).tar |