aboutsummaryrefslogtreecommitdiff
path: root/ide/idetop.ml
AgeCommit message (Expand)Author
2018-05-25Remove some occurrences of Evd.emptyMaxime Dénès
2018-05-21[ide] Remove special option `-ideslave`Emilio Jesus Gallego Arias
2018-05-21[stm] Make toplevels standalone executables.Emilio Jesus Gallego Arias