From 3b766fd8859b692e3e93cf83bf87d393e32c572e Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Thu, 3 Sep 2020 13:26:00 +0200
Subject: Merge numeral and string notation plugins

---
 Makefile.common | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'Makefile.common')

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
-- 
cgit v1.2.3