]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 8d1b8c3) | patch
When locate is used during the lexing phase, it may happen that no URI is
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 9 Sep 2002 10:10:37 +0000 (10:10 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 9 Sep 2002 10:10:37 +0000 (10:10 +0000)
commite34305aa0b9c8c9095e811b7ab720ffd4d283081
tree657a3dc7177f5adc96c29105fb151be14dcd43c4tree | snapshot
parent8d1b8c31da7bdfb695636bd4ef1c7c948ce511c4commit | diff
When locate is used during the lexing phase, it may happen that no URI is
found or more than an URI is found. In those cases a window is now opened
and the user is asked to either enter the URI (if none was found) or
choose from the list of found URIs.
helm/gTopLevel/gTopLevel.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.