diff --git a/doc/developer/Makefile b/doc/developer/Makefile index ab52d0e4172a463551bc077c473c1306fb0e39bc..4ce9e948e29de1c21f184f401c6168901f8de54d 100644 --- a/doc/developer/Makefile +++ b/doc/developer/Makefile @@ -49,7 +49,7 @@ else -load-script ./examples/acsl_extension \ -load-script ./hello_world/hello_world.ml \ | tee check.log - if grep -e "user error" check.log; then \ + if grep -e "User Error" check.log; then \ echo "Examples script do not compile with current Frama-C."; \ echo "Please examine check.log and make appropriate changes"; \ exit 1; \ diff --git a/doc/developer/examples/acsl_extension.ml b/doc/developer/examples/acsl_extension.ml index b4848615dd58d2c19e6d4e1bb5d098f0a820d044..9c677e002004f551f2cbfe95d296cdc3caa23997 100644 --- a/doc/developer/examples/acsl_extension.ml +++ b/doc/developer/examples/acsl_extension.ml @@ -14,4 +14,4 @@ let type_foo ~typing_context ~loc:_loc l = in Ext_terms res -let () = Logic_typing.register_behavior_extension "foo" type_foo +let () = Logic_typing.register_behavior_extension "foo" false type_foo