#!/bin/sh public_symbols_txt=$1 cat <