From e8a1f51b3fa848bf04fc13b5a33666e1856aab71 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Wed, 6 Jul 2005 15:03:41 +0000
Subject: [PATCH] check on baseuri

---
 helm/matita/matita.ma.templ | 2 +-
 helm/matita/matitaEngine.ml | 6 +++++-
 2 files changed, 6 insertions(+), 2 deletions(-)

diff --git a/helm/matita/matita.ma.templ b/helm/matita/matita.ma.templ
index 157c010d1..4fa107ce0 100644
--- a/helm/matita/matita.ma.templ
+++ b/helm/matita/matita.ma.templ
@@ -12,5 +12,5 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/<fill here>".
+set "baseuri" "cic:/matita/#fill here#".
 
diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index b20755d87..ebcf0538a 100644
--- a/helm/matita/matitaEngine.ml
+++ b/helm/matita/matitaEngine.ml
@@ -459,7 +459,11 @@ let eval_command status cmd =
   | TacticAst.Set (loc, name, value) -> 
       let value = 
         if name = "baseuri" then
-          MatitaMisc.strip_trailing_slash value
+          let v = MatitaMisc.strip_trailing_slash value in
+          try
+            ignore (String.index v ' ');
+            command_error "baseuri can't contain spaces"
+          with Not_found -> v
         else
           value
       in
-- 
2.39.2