Plugins don't belong to /usr/share

[SnarkBoojum]

While working on the Debian alt-ergo package, the tools complained:

E: alt-ergo: arch-dependent-file-in-usr-share usr/share/alt-ergo/plugins/AB-Why3-plugin.cmxs
E: alt-ergo: arch-dependent-file-in-usr-share usr/share/alt-ergo/plugins/fm-simplex-plugin.cmxs

and indeed, if those files are arch-dependent, they should go somewhere else ; perhaps in /usr/lib/alt-ergo ?