BTW, as a quick note, purely textual include should be doable with a simple wrapper script that invokes the c++ preprocessor frontend. (I can't remember why I didn't implement it as such at the time.)
On Sun, May 5, 2019 at 12:30 PM Martin Blais <bl...@furius.ca> wrote: > This is what I meant. By "disabling" I meant not silently ignoring, but > raise an error. > > > On Sun, May 5, 2019 at 12:26 PM Zhuoyun Wei <wzy...@wzyboy.org> wrote: > >> On Sun, May 5, 2019, at 20:51, francois PEGORY wrote: >> > According me , I think either : >> > 1) it is possible anywhere and it work as it was put in the main file. >> > Easy to explain , hard to implement. >> > >> > 2) if you put it in a file included, it raise a error. >> > The only question is which directive are reserved for the main file. >> > First thought , include and options >> > >> > What do you think ? >> > >> >> I'm with the second approach. Raising an error if any option directives >> are detected in included files is better than sliently ignoring the options >> and confusing (new) users. >> >> -- >> Zhuoyun Wei >> >> -- >> You received this message because you are subscribed to the Google Groups >> "Beancount" group. >> To unsubscribe from this group and stop receiving emails from it, send an >> email to beancount+unsubscr...@googlegroups.com. >> To post to this group, send email to beancount@googlegroups.com. >> To view this discussion on the web visit >> https://groups.google.com/d/msgid/beancount/42a9180e-d023-46f4-be0e-c8a66993b5b1%40www.fastmail.com >> . >> For more options, visit https://groups.google.com/d/optout. >> > -- You received this message because you are subscribed to the Google Groups "Beancount" group. To unsubscribe from this group and stop receiving emails from it, send an email to beancount+unsubscr...@googlegroups.com. To post to this group, send email to beancount@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/beancount/CAK21%2BhPFskJWgoQNzw3-2GLY03K94G3xFuU0P-vVG2aociLCwQ%40mail.gmail.com. For more options, visit https://groups.google.com/d/optout.
