diff options
| author | Kevin Quick <kquick@galois.com> | 2020-09-24 22:46:03 -0700 |
|---|---|---|
| committer | Kevin Quick <kquick@galois.com> | 2020-09-24 22:46:03 -0700 |
| commit | c2f48cfcee501dd15690245d481d154444456f66 (patch) | |
| tree | 2072b771611e7d70e5f032f19a1ca84e288b2231 /Makefile | |
| parent | a439e9488df6c13d0e44dd4816df98487d69f4c6 (diff) | |
Complete conversion of "url" to "host" with associated variable renaming.
Completes the change begun in commit 56f1e0d to consistently use the
"host" attribute for "github" and "gitlab" inputs instead of a "url"
attribute.
Diffstat (limited to 'Makefile')
0 files changed, 0 insertions, 0 deletions