theRestartScriptHeader  136 dmtcp_coordinator.cpp static const char* theRestartScriptHeader =
theRestartScriptHeader 1395 dmtcp_coordinator.cpp   fprintf ( fp, "%s", theRestartScriptHeader );