2017-11-25 06:10:26 +00:00
|
|
|
option('browser_plugin',
|
2017-05-25 00:16:27 +00:00
|
|
|
type: 'boolean',
|
|
|
|
value: true,
|
|
|
|
description: 'Enable extensions.gnome.org browser plugin'
|
|
|
|
)
|
|
|
|
|
2017-11-25 06:10:26 +00:00
|
|
|
option('gtk_doc',
|
2017-05-25 00:16:27 +00:00
|
|
|
type: 'boolean',
|
|
|
|
value: false,
|
|
|
|
description: 'Build API reference'
|
|
|
|
)
|
|
|
|
|
2017-11-25 06:10:26 +00:00
|
|
|
option('man',
|
2017-05-25 00:16:27 +00:00
|
|
|
type: 'boolean',
|
|
|
|
value: true,
|
|
|
|
description: 'Generate man pages'
|
|
|
|
)
|
|
|
|
|
2017-11-25 06:10:26 +00:00
|
|
|
option('networkmanager',
|
2017-11-25 06:15:39 +00:00
|
|
|
type: 'boolean',
|
|
|
|
value: true,
|
2017-05-25 00:16:27 +00:00
|
|
|
description: 'Enable NetworkManager support'
|
|
|
|
)
|
|
|
|
|
2017-11-25 06:10:26 +00:00
|
|
|
option('systemd',
|
2017-11-25 06:15:39 +00:00
|
|
|
type: 'boolean',
|
|
|
|
value: true,
|
2017-05-25 00:16:27 +00:00
|
|
|
description: 'Enable systemd integration'
|
|
|
|
)
|