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 6208685199..28ab304c2e 100644 --- a/Makefile.common +++ b/Makefile.common @@ -388,9 +388,9 @@ COQIDECMO:=ide/utils/okey.cmo ide/utils/config_file.cmo \ ide/utils/configwin_messages.cmo ide/utils/configwin_ihm.cmo \ ide/utils/configwin.cmo \ ide/utils/editable_cells.cmo ide/config_parser.cmo \ + ide/typed_notebook.cmo \ ide/config_lexer.cmo ide/utf8_convert.cmo ide/preferences.cmo \ ide/ideutils.cmo ide/blaster_window.cmo ide/undo.cmo \ - ide/find_phrase.cmo \ ide/highlight.cmo ide/coq.cmo ide/coq_commands.cmo \ ide/coq_tactics.cmo ide/command_windows.cmo ide/coqide.cmo |