7fee59
Update manual_updateOutputFiles.sh to remove extension from manual's base filename. This way it is possible to create different files using the same name but different extensions.