You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Right now, when Roosterize suggests lemma names for a complete project, that project has to be built first (usually using make in it root directory). However, it would be more intuitive to pass a build command to Roosterize than build the project separately.
For example, one could introduce a buildcmd command-line option, used as follows:
Right now, when Roosterize suggests lemma names for a complete project, that project has to be built first (usually using
make
in it root directory). However, it would be more intuitive to pass a build command to Roosterize than build the project separately.For example, one could introduce a
buildcmd
command-line option, used as follows:The text was updated successfully, but these errors were encountered: