How to split timestamp and put a dot between YYYYMMDD and HHMMSS?

Shell Programming and Scripting
1

I have a string

time=20170303201234

I want to split it and put a dot
result:

20170303.201234

CODE:

ttdotss=`echo ${time} | [0-9]{8}.[0-9]{8}`

Doesn't understand
I tried this:

CODE:

ttdotss=`echo ${time} |cut -c 1-8 | . | cut -c 9-14`

Result:

 script[69]: .: argument expected

Could you help me?

Thanks form contribution

2 
echo '20170303201234' | sed 's/\(.*\)\(......\)/\1.\2/'
3

sed:

echo "$time" | sed 's/......$/.&/'

If you have ksh93 , or zsh , try:

printf "%.6f\n" "$(( time / 1000000.0 ))"

--
just for fun:

echo "$time" | fold -w8 | paste -d\. - -
1 Like
4

Found
Code:

 
 ttdotss=`echo ${time} |sed 's/.\{8\}/&./g'`

Result

 
 20170303.122334
5 
echo ${time%??????}.${time#????????}
20170303.201234