>Are not the opt_*.h files produced by "defopt file OPTION" always
>created?  If so then is it necessary to run "make depend" after every
>config? 

Yes, and (to be always safe) yes. 

It's OK if you only rerun make config once, but if you change options
and rerun config more than once, you can still get hosed.  Suppose you
start with an up-to-date .depend:

Step 1: Add some options whcih add new .o files.
        run config but not make depend.
 	Okay so far.

Step 2: Add yet more options, which change some opt_*.h files used by
        the new .o files added in step 2.  .depend _doesn't_
	know about those dependences, so it doens't rebuild the
	.o files added in step #1.  Ooops.


>It would be nice if options(4) mentioned which options were defopt'ed
>and suggested hint about ``make depend'' in whichever way is correct.
>Should I send-pr this suggestion to act as a reminder?  ;-)

Yes, please do. Most documented options are now defopt'ed, so it may
make more sense to note the options which _aren't_ (though may be more
work to keep up-to-date that way).