Changes

Summary

1. make disable popup option available to all frontends (details)

Commit 0079c74d55caaf731e702e830839a799aaa4ab67 by Vincent Sanders make disable popup option available to all frontends
	frontends/gtk/options.h (diff)
	frontends/monkey/options.h (diff)
	frontends/riscos/options.h (diff)
	frontends/riscos/configure/con_content.c (diff)
	desktop/options.h (diff)
	test/data/Choices-all (diff)