From 9037b899d25db7e09e90e9b4689f073f0dc4c729 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 15 Jul 2005 23:39:10 +0000 Subject: [PATCH] fixed a specific case in development handling --- helm/matita/matitaScript.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml index 4f6627fcd..4a6115813 100644 --- a/helm/matita/matitaScript.ml +++ b/helm/matita/matitaScript.ml @@ -78,7 +78,7 @@ let eval_with_engine guistuff status user_goal parsed_text st = let module TAPp = TacticAstPp in let include_ = match guistuff.filenamedata with - | _,None -> [] + | None,None -> [] | None,Some devel -> [MatitamakeLib.root_for_development devel ] | Some f,_ -> match MatitamakeLib.development_for_dir (Filename.dirname f) with -- 2.39.2