]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 531db3a) | patch
bugfix when user query contains metas: their context should not be analyzed
authorStefano Zacchiroli <zack@upsilon.cc>
Tue, 15 Mar 2005 08:21:56 +0000 (08:21 +0000)
committerStefano Zacchiroli <zack@upsilon.cc>
Tue, 15 Mar 2005 08:21:56 +0000 (08:21 +0000)
commit74682761ea8bf251be5b599e3ac28ec0d95f0958
treea5762b10cd193b9ca83f64e37885f395a6e27b6ctree | snapshot
parent531db3a11c2faa55884c490443d56ac308f9ac9fcommit | diff
bugfix when user query contains metas: their context should not be analyzed
as it were in main position
helm/ocaml/metadata/metadataExtractor.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.