FilePath.get_extension behaviour for files with leading dots is counter-intuitive

[dmbaturin]

If a file name starts with a dot and doesn't have any more dots, FilePath.get_extension considers it a file with an empty name but with an extension.

utop # FilePath.get_extension ".bashrc" ;;
- : string = "bashrc"

I believe when asked, most people will say that a file like .bashrc is a file with no extension, and that a leading dot is a part of the file name. .bashrc.gz is a file named .bashrc with extension gz.