Fix compile error on kernel 4 13#16

rodrigosiqueira wants to merge 3 commits intoproject-dune:masterproject-dune/dune:masterfrom

rodrigosiqueira:fix_compile_error_on_kernel_4_13rodrigosiqueira/dune-1:fix_compile_error_on_kernel_4_13Copy head branch name to clipboard