Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Filename.get_suffix is needed (3.11.2, but 4.0.x does also not contain it) #5807

Closed
vicuna opened this issue Nov 3, 2012 · 5 comments
Closed

Comments

@vicuna
Copy link

vicuna commented Nov 3, 2012

Original bug ID: 5807
Reporter: oliver
Assigned to: @alainfrisch
Status: resolved (set by @alainfrisch on 2016-12-08T10:44:47Z)
Resolution: fixed
Priority: normal
Severity: feature
Version: 3.11.2
Fixed in version: 4.04.0
Category: standard library
Tags: patch, junior_job

Bug description

In module Filename there is

  • "check_suffix" to check on a known suffix

  • "chop_suffix" to chop a known suffix

  • "chop_extension" to chop any (even unknown) extension

For working on files with any file extension
(previously unknown, means: not looking for a specific extension/suffix),
to use "check_suffix" and "chop_suffix" a "Filename.get_suffix"
function would help a lot.

"chop_extension" could then be implemented
comparingly easily with "get_suffix" and "chop_suffix".

But to extract the suffix from the filename
is annoying stuff that needs String-module or a for-loop.
But not seldom, it's needed to extract the extension from a file.
above,

So all in all, a Filename.get_suffix would be helpful in any case.

Steps to reproduce

./.

Additional information

./.

File attachments

@vicuna
Copy link
Author

vicuna commented Jun 20, 2013

Comment author: @damiendoligez

Two remarks:

  1. It should be called get_extension, not get_suffix.
  2. If the file name contains more than one dot, it should return the smallest extension.

@vicuna
Copy link
Author

vicuna commented Jul 30, 2013

Comment author: mcclurmc

Patch uploaded.

@vicuna
Copy link
Author

vicuna commented Jul 30, 2013

Comment author: euanh

Gah, beaten to it!!! Uploaded alternative patch PR-5807_alt.patch, pair-programmed with jludlam. :)

@vicuna
Copy link
Author

vicuna commented Dec 16, 2013

Comment author: @damiendoligez

In fact it's easy (if rather unelegant) to define it using chop_extension :

let get_extension n =
let l = String.length (chop_extension n) in
String.sub n l (String.length n - l)
;;

@vicuna
Copy link
Author

vicuna commented Dec 8, 2016

Comment author: @alainfrisch

Filename.extension added to 4.04.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

2 participants