]> matita.cs.unibo.it Git - helm.git/commit
changed "locate" so that it supports shell-like pattern matching with
authorStefano Zacchiroli <zack@upsilon.cc>
Fri, 3 Dec 2004 16:04:01 +0000 (16:04 +0000)
committerStefano Zacchiroli <zack@upsilon.cc>
Fri, 3 Dec 2004 16:04:01 +0000 (16:04 +0000)
commit6c6530f435e82cc7688c3f76c4d61b4e0bd7a0e5
treeca2db0f5767eb37597529e5f45c1008a12043f55
parent301e61627dc24ebc027d5f2dd990f738a1ac65b7
changed "locate" so that it supports shell-like pattern matching with
'*' and '?' wildcards
helm/ocaml/tactics/metadataQuery.ml
helm/ocaml/tactics/metadataQuery.mli