On 14:13 12 Feb 2002, Wojtek Pilorz <[EMAIL PROTECTED]> wrote:
| > | If we want bash-only solution we can use a bit faster (no subprocessed
| > | created):
| > | for f in *.pc; do newname="${f%.pc}".jpg; mv -i "$f" "$newname"; done
| >
| > True, and will fail badly on a system without bash. (And
On Tue, 12 Feb 2002, Cameron Simpson wrote:
> On 08:38 12 Feb 2002, Wojtek Pilorz <[EMAIL PROTECTED]> wrote:
> | On Tue, 12 Feb 2002, Cameron Simpson wrote:
[...]
> | > for f in *.pc
> | > do newname=`basename "$f" .bc`.jpg
> | > mv -i "$f" "$newname"
> | > done
> | It seems that you try to
> Message: 13
> From: "Reuben D Budiardja" <[EMAIL PROTECTED]>
> To: [EMAIL PROTECTED]
> Subject: Change file extension using bash (OT)
> Date: Mon, 11 Feb 2002 23:39:10 -0500
> Reply-To: [EMAIL PROTECTED]
>
>
> Hi,
> I need a bit of help with
On 08:38 12 Feb 2002, Wojtek Pilorz <[EMAIL PROTECTED]> wrote:
| On Tue, 12 Feb 2002, Cameron Simpson wrote:
| > On 23:39 11 Feb 2002, Reuben D Budiardja <[EMAIL PROTECTED]> wrote:
| > | I need a bit of help with bash here. I try to create a script that would
| > | change the extension of files i
On Mon, Feb 11, 2002 at 11:39:10PM -0500, Reuben D Budiardja wrote:
>
> I need a bit of help with bash here. I try to create a script that would
> change the extension of files in directory. I have files like
> xxx.pc that I want a change to xxx.jpg, where xxx is numbers, in a directory.
> How
On Tue, 12 Feb 2002, Cameron Simpson wrote:
> Date: Tue, 12 Feb 2002 15:51:10 +1100
> From: Cameron Simpson <[EMAIL PROTECTED]>
> Reply-To: [EMAIL PROTECTED]
> To: [EMAIL PROTECTED]
> Subject: Re: Change file extension using bash (OT)
>
> On 23:39 11 Feb 2002,
On 23:39 11 Feb 2002, Reuben D Budiardja <[EMAIL PROTECTED]> wrote:
| I need a bit of help with bash here. I try to create a script that would
| change the extension of files in directory. I have files like
| xxx.pc that I want a change to xxx.jpg, where xxx is numbers, in a directory.
| How ca
Hi,
I need a bit of help with bash here. I try to create a script that would
change the extension of files in directory. I have files like
xxx.pc that I want a change to xxx.jpg, where xxx is numbers, in a directory.
How can I do that using bash?
thanks for any help.
Reuben D.B.
__
