diff options
| author | Emilio Jesus Gallego Arias | 2017-05-30 18:47:27 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2017-05-30 23:55:45 +0200 |
| commit | 6c41cad1871b82696db3df6bf5ce62277fc82e92 (patch) | |
| tree | 24bde160d6e9aab772d31c41770d97d2d5a1fa0b /dev | |
| parent | fd36c0451c26e44b1b7e93299d3367ad2d35fee3 (diff) | |
[ide] Correct merging error.
There was a mistake in the conflict resolution of merge
6f2c19a1054ce58927dfa5b33131c3665fd5fdf8 which wrongly undid the the
deletion of the file `ide/texmacspp.ml` in 6a412da , fixing here and
sorry for the problem.
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions