diff --git a/src/config.xml b/src/config.xml index 726183c6197..92da3cab5fe 100644 --- a/src/config.xml +++ b/src/config.xml @@ -2492,10 +2492,19 @@ EXTRA_SEARCH_MAPPINGS = tagname1=loc1 tagname2=loc2 ...