Why is MAX_NUM_FREEMEM_REG defined in two different places?

seL4 kernel
1

It seems like MAX_NUM_FREEMEM_REG is defined in bootinfo.h and boot.h(which includesbootinfo.h`.

Is there a reason for having it define din both places? It is somewhat inconvenient when you need to change it.

Thanks!

2

I can’t see any reason. Probably copy + paste error from the last boot refactor we did. Clean away :).

1 Like
3

I think the intention was for the common definition in kernel/boot.h to have been removed.

4

You’re like a mind reader… was about to ask which one should go :slight_smile:

1 Like
5
1 Like