improved distr entry
This commit is contained in:
parent
dc7180fb8f
commit
56b8473042
@ -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…
x
Reference in New Issue
Block a user