diff options
| author | Paul Zimmermann <Paul.Zimmermann@inria.fr> | 2018-04-18 16:31:31 +0200 |
|---|---|---|
| committer | Paul Zimmermann <Paul.Zimmermann@inria.fr> | 2018-04-18 16:31:31 +0200 |
| commit | 8928e15335491f4ee9230e49bd88a59f4c2b2c36 (patch) | |
| tree | 20fc2a402e8e064a79b2ee85c81c8477898ebecc | |
| parent | 438e8453e5bdd99a5959ca284733c4e28758af47 (diff) | |
| download | mpc-git-8928e15335491f4ee9230e49bd88a59f4c2b2c36.tar.gz | |
tools/coverage should be executable
| -rwxr-xr-x[-rw-r--r--] | tools/coverage | 0 |
1 files changed, 0 insertions, 0 deletions
diff --git a/tools/coverage b/tools/coverage index 5bc4c3c..5bc4c3c 100644..100755 --- a/tools/coverage +++ b/tools/coverage |