diff options
Diffstat (limited to 'Makefile.common')
| -rw-r--r-- | Makefile.common | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Makefile.common b/Makefile.common index db78a65ed..2eff24fcf 100644 --- a/Makefile.common +++ b/Makefile.common @@ -367,7 +367,7 @@ COQIDECMO:=\ $(addprefix ide/, \ config_parser.cmo typed_notebook.cmo config_lexer.cmo \ utf8_convert.cmo preferences.cmo ideutils.cmo \ - blaster_window.cmo undo.cmo highlight.cmo \ + gtk_parsing.cmo undo.cmo highlight.cmo \ coq.cmo coq_commands.cmo coq_tactics.cmo \ command_windows.cmo coqide.cmo ) |