equal
deleted
inserted
replaced
176 title = "Location", key = "country", width = 2; |
176 title = "Location", key = "country", width = 2; |
177 }); |
177 }); |
178 end |
178 end |
179 end |
179 end |
180 |
180 |
181 local width = tonumber(os.getenv("COLUMNS")) or 80; |
181 local row, width = require "util.human.io".table(colspec); |
182 local row = require "util.human.io".table(colspec, width); |
|
183 |
182 |
184 print(string.rep("-", width)); |
183 print(string.rep("-", width)); |
185 print(row()); |
184 print(row()); |
186 print(string.rep("-", width)); |
185 print(string.rep("-", width)); |
187 for _, entry, when, user in results do |
186 for _, entry, when, user in results do |