From 4da839f5ce657df25701d92122bdf0bc88e93298 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Tue, 26 Nov 2019 16:13:26 +0100
Subject: [PATCH] [server] Fixes syntax constraints for creating new data
 names.

Data names had to be dash-separated list of lowercase identifiers and also
start by "plugin.", which was incompatible.
---
 src/plugins/server/syntax.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/plugins/server/syntax.ml b/src/plugins/server/syntax.ml
index 41d2b8e45ff..f36e96261b9 100644
--- a/src/plugins/server/syntax.ml
+++ b/src/plugins/server/syntax.ml
@@ -30,7 +30,7 @@ let check_plugin plugin name =
   let k = String.length plugin in
   if not (String.length name > k &&
           String.sub n 0 k = p &&
-          String.get n k = '.')
+          String.get n k = '-')
   then
     Senv.warning ~wkey:Senv.wpage
       "Data %S shall be named « %s-* »"
-- 
GitLab