diff options
| author | Christian Grothoff <christian@grothoff.org> | 2019-12-15 12:44:16 +0100 |
|---|---|---|
| committer | Christian Grothoff <christian@grothoff.org> | 2019-12-15 12:44:16 +0100 |
| commit | 9eff97869cc14bbae345db62a8b34f8161541ca1 (patch) | |
| tree | b53c25bc12c3882037f695e65bfcdd877f67ac82 | |
| parent | 1fc603800cf092e0d5750caf01ec46335109cb7f (diff) | |
mark as executable
| -rwxr-xr-x[-rw-r--r--] | contrib/coverage.sh | 0 |
1 files changed, 0 insertions, 0 deletions
diff --git a/contrib/coverage.sh b/contrib/coverage.sh index cce622283..cce622283 100644..100755 --- a/contrib/coverage.sh +++ b/contrib/coverage.sh |