fetchInto($row)) { echo "\n"; foreach ($keys as $key) { if ( isset($_POST[$key]) ) { $data[$key]=array_shift($row); echo "\n"; } } echo "

".$key."

";
		if ( $key=="submit_ts" || $key=="start_ts" || $key=="end_ts" )
		  {
		    echo date("Y-m-d H:i:s",$data[$key]);
		  }
		else
		  {
		    echo htmlspecialchars($data[$key]);
		  }
		echo "

\n"; } db_disconnect($db); bookmarkable_url(); } else { begin_form("jobinfo.php"); text_field("Job id","jobid",8); system_chooser(); checkboxes_from_array("Properties",$props); end_form(); } page_footer(); ?>