[][src]Constant agda_mode::agda::INTERACTION_COMMAND

pub const INTERACTION_COMMAND: &str = "--interaction-json";