alainfrisch aa4f427591 Add Filename.extension and Filename.remove_extension. ... The definition was suggested by Daniel Bunzli. It considers that ".", "..", ".foo" all have an empty extension. This commit also fixes chop_extension to align with this definition and adds remove_extension which behaves as chop_extension but does not fail when the extension is empty. There used to be a Misc.chop_extension_if_any in the compiler code base. The commit also replaces it with the new Filename.remove_extension.		2016-07-10 00:16:48 +02:00
..
doligez	Update headers for the new license.	2016-02-18 16:59:16 +01:00
frisch	Add Filename.extension and Filename.remove_extension.	2016-07-10 00:16:48 +02:00
garrigue	Call the '#' sign hash rather than sharp.	2016-05-09 16:34:40 +02:00