improved distr entry
This commit is contained in:
parent
15cf912949
commit
3b32a79997
|
@ -112,6 +112,8 @@ opr:
|
|||
make pr | opr
|
||||
|
||||
distr: .distr
|
||||
(cd switch; make distr)
|
||||
(cd test; make distr)
|
||||
|
||||
.distr: Makefile
|
||||
echo $(DISTR) | tr ' ' '\012' >.distr
|
||||
|
|
Loading…
Reference in a new issue