Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0005807OCamlOCaml standard librarypublic2012-11-03 01:222013-12-16 13:31
Reporteroliver 
Assigned To 
PrioritynormalSeverityfeatureReproducibilityalways
StatusconfirmedResolutionopen 
PlatformOSOS Version
Product Version3.11.2 
Target VersionFixed in Version 
Summary0005807: Filename.get_suffix is needed (3.11.2, but 4.0.x does also not contain it)
DescriptionIn 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./.
Tagsjunior_job, patch
Attached Filespatch file icon 0001-Fix-PR-5807-add-function-Filename.extension.patch [^] (1,985 bytes) 2013-07-30 20:05 [Show Content]
patch file icon PR-5807_alt.patch [^] (2,025 bytes) 2013-07-30 22:10 [Show Content]

- Relationships

-  Notes
(0009585)
doligez (administrator)
2013-06-20 10:33

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.

(0010012)
mcclurmc (reporter)
2013-07-30 20:05

Patch uploaded.
(0010017)
euanh (reporter)
2013-07-30 20:33
edited on: 2013-07-30 22:09

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

(0010718)
doligez (administrator)
2013-12-16 13:31

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)
;;

- Issue History
Date Modified Username Field Change
2012-11-03 01:22 oliver New Issue
2013-06-20 10:33 doligez Note Added: 0009585
2013-06-20 10:33 doligez Status new => confirmed
2013-07-28 23:42 gasche Tag Attached: junior_job
2013-07-30 20:05 mcclurmc File Added: 0001-Fix-PR-5807-add-function-Filename.extension.patch
2013-07-30 20:05 mcclurmc Note Added: 0010012
2013-07-30 20:31 euanh File Added: PR-5807-alt.patch
2013-07-30 20:33 euanh Note Added: 0010017
2013-07-30 22:09 euanh Note Edited: 0010017 View Revisions
2013-07-30 22:10 euanh File Added: PR-5807_alt.patch
2013-07-30 22:13 lpw25 File Deleted: PR-5807-alt.patch
2013-09-09 00:43 lpw25 Tag Attached: patch
2013-12-16 13:31 doligez Note Added: 0010718


Copyright © 2000 - 2011 MantisBT Group
Powered by Mantis Bugtracker