#!/bin/sh

# Insert an extra space after column 4:
awk '/^   / { print } !/^   / {print substr($0,0,4) " " substr($0,5)}' |

# This does all the work:
awk -f ../tools/mk_tables.awk