#! /bin/bash
# Last edited on 2007-01-27 14:38:29 by stolfi

# Usage: split-joined-sources {BIGFILE}

# The {BIGFILE} should have been created by join-sources-for-editing.
# Parses {BIGFILE} into its constituent files, and writes each file
# using the filename specified by the "// #FILE " line that just
# precedes it. Also undoes some changes to timestamps and 
# "#include"s that were introduced by join-sources-for-editing.
# Fails if a filename in the file belongs in a non-existing or
# protected directory.

cat $1 \
  | sed \
     -e 's:// [\#]FILE *:#FILE :g' \
     -e 's:// *\([~][~][~]*\)$:\1:g' \
     -e 's:// [\#]INCLUDE *<\([A-Z]\):#include <\1:g' \
     -e 's:// [\#]TIMESTAMP *::g' \
  | splitsep