Hello, I just added a new symbol to libgmpxx. Should I touch one of the LIBGMPXX_LT_* in Makefile.am, mark somewhere that it may need to be done prior to release, or ignore the (non-)issue? -- Marc Glisse