+ system("/bin/rm -rf '$tmpdir/$dirname'");
+}
+
+# like make_tar above, except it includes a copy of code/wfpl
+function make_wfpl_tar($dirname, $files) {
+ make_tar($dirname, $files, 'add_wfpl_dir');
+}
+
+function add_wfpl_dir($dir) {
+ mkdir("$dir/code");
+ system("/bin/cp -HRp 'code/wfpl' '$dir/code/'", $return_code);
+ if($return_code != 0) {
+ die("ERROR: while trying to copy wfpl into archive: cp returned $return_code");