From e559e715e8ce9d2f4de6e8af4c9c7d4f3609de91 Mon Sep 17 00:00:00 2001
From: Olivier Laurent
Date: Wed, 29 Apr 2020 09:49:06 +0200
Subject: correct script name create_overlays.sh

---
 dev/ci/README-developers.md | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'dev')

diff --git a/dev/ci/README-developers.md b/dev/ci/README-developers.md
index 6a740b9033..88d08a1724 100644
--- a/dev/ci/README-developers.md
+++ b/dev/ci/README-developers.md
@@ -72,10 +72,10 @@ Moreover your PR must absolutely update the [`CHANGES.md`](../../CHANGES.md) fil
 ### Experimental automatic overlay creation and building
 
 If you break external projects that are hosted on GitHub, you can use
-the `create-overlays.sh` script to automatically perform most of the
+the `create_overlays.sh` script to automatically perform most of the
 above steps. In order to do so, call the script as:
 ```
-./dev/tools/create-overlays.sh ejgallego 9873 aac_tactics elpi ltac
+./dev/tools/create_overlays.sh ejgallego 9873 aac_tactics elpi ltac
 ```
 replacing `ejgallego` by your GitHub nickname and `9873` by the actual PR
 number. The script will:
-- 
cgit v1.2.3