#! /bin/bash
# Last edited on 2007-01-23 17:56:53 by stolfi

# Usage: list-joined-sources {BIGFILE}

# The {BIGFILE} should have been created by join-sources-for-editing.
# This script writes to standard output the filenames of the files contained
# in {BIGFILE}, one per line, in the order they appear

cat $1 \
  | egrep -e '^[\/][\/] *[\#]FILE ' \
  | sed \
      -e 's:// [\#]FILE *::g' \
      -e 's:[ ]*$::g' \
      -e '/^$/d'