Converting time format - mIRC Discussion Forums

Is there a simple way to convert the following time format:

2:30

to

14:30 ?

I need the smallest, easiest way to do this. Use of an identifier would be great.

$time(HH:nn)

That doesn't do what I want...

My script prompts a user to enter standard time. After the user enters a time, I need my script to convert it to military format.

For example, a user may enter 3:45 PM. The script would convert 3:45 to 15:45.

I was hoping there was a simple identifier that would do this.

I had something lying around that did this, I made it ages ago so the code's a bit messy, but it works.

Code:

alias convtime {
  if ($gettok($1,2,32)) {
    if ($ifmatch == AM) { return $gettok($1,1,32) }
    elseif ($ifmatch == PM) { return $gettok($calc($mid($1,1,$calc($pos($1,:,1) - 1)) + 12) $+ : $+ $mid($1,$calc($pos($1,:,1) + 1)),1,32) }
  }
  else {
    if ($mid($1,1,$calc($pos($1,:,1) - 1)) &gt; 12) { return $calc($mid($1,1,$calc($pos($1,:,1) - 1)) - 12) $+ : $+ $mid($1,$calc($pos($1,:,1) + 1)) PM }
    else { return $1 AM }
  }
}

$convtime(11:00 AM) = 11:00
$convtime(11:00 PM) = 23:00
$convtime(11:00) = 11:00 AM
$convtime(23:00) = 11:00 PM

Code:

alias convert.time { var %a = $ctime($date $remove($1-,$chr(32))) | return $time(%a,HH:nn) }

//echo -a $convert.time(1:00 PM)
13:00

//echo -a $convert.time(1:00 AM)
01:00

Thanks! Nice and small, and it works great!