diff options
Diffstat (limited to 'Makefile.common')
| -rw-r--r-- | Makefile.common | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/Makefile.common b/Makefile.common index 29020dc4ad..caf1821ce5 100644 --- a/Makefile.common +++ b/Makefile.common @@ -151,8 +151,7 @@ RTAUTOCMO:=plugins/rtauto/rtauto_plugin.cmo SYNTAXCMO:=$(addprefix plugins/syntax/, \ int63_syntax_plugin.cmo \ float_syntax_plugin.cmo \ - numeral_notation_plugin.cmo \ - string_notation_plugin.cmo) + number_string_notation_plugin.cmo) DERIVECMO:=plugins/derive/derive_plugin.cmo LTACCMO:=plugins/ltac/ltac_plugin.cmo plugins/ltac/tauto_plugin.cmo SSRMATCHINGCMO:=plugins/ssrmatching/ssrmatching_plugin.cmo |