aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools/fake_ide.ml
Commit message (Expand)AuthorAge
* Fix test-suite/ide for repository compiled without -local (fix #2600)Gravatar letouzey2011-09-19
* fake_ide: a short program to mimic an ide talking to coqtop -ideslaveGravatar letouzey2011-09-05