#!/bin/sh -x time-stats sum 00before/*.time >00before.txt time-stats sum 00after/*.time >00after.txt time-stats sum DLV/00before/*.time >DLV/00before.txt time-stats sum DLV/00after/*.time >DLV/00after.txt time-stats sum MICO/00before/*.time >MICO/00before.txt time-stats sum MICO/00after/*.time >MICO/00after.txt time-stats sum SPEC2000/00before/*.time >SPEC2000/00before.txt time-stats sum SPEC2000/00after/*.time >SPEC2000/00after.txt time-stats sum TRAMP3D/00before/*.time >TRAMP3D/00before.txt time-stats sum TRAMP3D/00after/*.time >TRAMP3D/00after.txt time-stats sum VARIOUS/00before/*.time >VARIOUS/00before.txt time-stats sum VARIOUS/00after/*.time >VARIOUS/00after.txt