max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix(library/tactic/vm_monitor): compilation warning

Browse source
This commit is contained in:
Leonardo de Moura 2017-03-22 07:40:16 -07:00
parent f9854be13f
commit c541f90d5b
1 changed files with 2 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/library/tactic/vm_monitor.cpp
View file

@ -435,7 +435,8 @@ void initialize_vm_monitor() {
register_system_attribute(basic_attribute(
"vm_monitor", "Registers a new virtual machine monitor. The annotated definition must be the of type "
"`vm_monitor S`. The command will override the last monitor.",
[](environment const & env, io_state const &, name const & n, unsigned, bool persistent) {
[](environment const & env, io_state const &, name const & n, unsigned, bool /* persistent */) {
/* Remark: We are currently ignoring the 'local' (i.e., persistent == false) modifier */
return vm_monitor_register(env, n);
}));