[boost] [filesystem] change_extension vs replace_extension: bug in the documentation or in the implementation