1 files changed, 1 insertions, 1 deletions

diff --git a/documentation/dev-manual/devtool.rst b/documentation/dev-manual/devtool.rst
index 2f17d50930..c82dc9c333 100644
--- a/documentation/dev-manual/devtool.rst
+++ b/documentation/dev-manual/devtool.rst
@@ -552,7 +552,7 @@ the two modes:
 
       This instance of VSCode uses plugins that are useful for the development
       of the application. ``devtool ide-sdk`` generates the necessary
-      ``extensions.json``, ``settings.json``, ``tasks.json``and ``launch.json``
+      ``extensions.json``, ``settings.json``, ``tasks.json`` and ``launch.json``
       configuration files for all the involved plugins.
 
       When the source code folder present in the workspace folder is opened in