diff options
| author | Miles Bader <miles@gnu.org> | 1995-10-07 00:17:04 +0000 |
|---|---|---|
| committer | Miles Bader <miles@gnu.org> | 1995-10-07 00:17:04 +0000 |
| commit | 14ff0be4a00ca32f7f0935d040a1ccd17209ec0e (patch) | |
| tree | e7998a8fc5894000da94e30dcb996cba40ae31e8 /benchmarks | |
| parent | ea284b0517d36658d6dcf7af30949651a2646752 (diff) | |
(OPT_BOOTFLAGS, OPT_EXEC_SERVER_TASK, OPT_HOST_PRIV_PORT,
OPT_DEVICE_MASTER_PORT): New defines.
(std_long_opts, parse_std_startup_opt): Add the --device-master-port,
--host-priv-port, --exec-server-task, and --bootflags options.
Diffstat (limited to 'benchmarks')
0 files changed, 0 insertions, 0 deletions