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

Comments

Projects
None yet
2 participants
@vicuna
Copy link
Collaborator

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

This comment has been minimized.

Copy link
Collaborator Author

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

This comment has been minimized.

Copy link
Collaborator Author

commented Jul 30, 2013

Comment author: mcclurmc

Patch uploaded.

@vicuna

This comment has been minimized.

Copy link
Collaborator Author

commented Jul 30, 2013

Comment author: euanh

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

@vicuna

This comment has been minimized.

Copy link
Collaborator Author

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

This comment has been minimized.

Copy link
Collaborator Author

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
You can’t perform that action at this time.