#include "config.h"
#include <stdio.h>
#include <string.h>

int main(int argc, char* argv[]) {
    size_t n_non_digits = strcspn(HOST_OS, "0123456789");
    printf("%s-%s-%.*s\n", HOST_CPU, HOST_VENDOR, n_non_digits, HOST_OS);
}