tools: Fix make dist

Missing bits of b45a1df5deadb029dcbe4522f0116d34f1cd2f1e
1 file changed