janestreet / jenga

Build system
90 stars 12 forks source link

Rename Path.basename to Path.filename #12

Open pippijn opened 9 years ago

pippijn commented 9 years ago

In GNU Make, basename means "path with its last extension stripped". In build systems, that is a common thing to operate on, and I'd like to call it "basename".

It does make sense to call it Path.basename, because of the basename(1) utility, but I think getting the "file name" from a path is semantically clearer, and reserves the word "basename" for the gmake meaning.