Ctrl-g to interrupt searches
commit320b6c24266850befac6efa0343b96606f2d7ada
authormalc <av1474@comtv.ru>
Thu, 8 Jul 2010 19:12:51 +0000 (8 23:12 +0400)
committermalc <av1474@comtv.ru>
Thu, 8 Jul 2010 19:12:51 +0000 (8 23:12 +0400)
tree2b5c050c9ce49bd912fb220e5c5710c8a3717b86
parent547706df4812781efea0b883392685aea26bfebe
Ctrl-g to interrupt searches
main.ml