diff options
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). |