]> matita.cs.unibo.it Git - helm.git/commitdiff
Dead code removed.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 28 Nov 2007 22:29:16 +0000 (22:29 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 28 Nov 2007 22:29:16 +0000 (22:29 +0000)
helm/software/matita/matitacLib.ml

index bed0819db85d0bfe20a9427bf7659d1a75aaf432..316d0f9f675ef9d78a168c03b33734b9d609fb23 100644 (file)
@@ -305,8 +305,7 @@ let main ~mode =
   (* must be called after init since args are set by cmdline parsing *)
   let fname = fname () in
   if false then
-   (let basename = Filename.basename (Filename.chop_extension fname) in
-   let baseuri =
+   (let baseuri =
     (* This does not work yet :-(
        let baseuri =
         GrafiteTypes.get_string_option