diff options
| author | Enrico Tassi | 2020-12-13 21:20:05 +0100 |
|---|---|---|
| committer | GitHub | 2020-12-13 21:20:05 +0100 |
| commit | 1c667f5c1caf828f7dbf3e9c7910b8a0b7b84d03 (patch) | |
| tree | b6c642cb8ebb03d77581815b2f144f0fabafcd88 /dev/ci | |
| parent | b927bb3eb66ceee8b80c91b2edf8894dc3fba79e (diff) | |
Update dev/ci/user-overlays/README.md
Co-authored-by: Théo Zimmermann <theo.zimmi@gmail.com>
Diffstat (limited to 'dev/ci')
| -rw-r--r-- | dev/ci/user-overlays/README.md | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/dev/ci/user-overlays/README.md b/dev/ci/user-overlays/README.md index da0cee09a2..cf1d71c1cd 100644 --- a/dev/ci/user-overlays/README.md +++ b/dev/ci/user-overlays/README.md @@ -25,7 +25,7 @@ overlay elpi https://github.com/SkySkimmer/coq-elpi noinstance 13128 ``` Such a file can be created automatically using the scripts -[`create_overlays.sh`]()../../dev/tools/create_overlays.sh). +[`create_overlays.sh`](../../dev/tools/create_overlays.sh). See also the list of projects for which one can write an overlay in the file [`ci-basic-overlay.sh`](../ci-basic-overlay.sh). |